HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem imp3a 361
Description: Importation deduction.
Hypothesis
Ref Expression
imp3.1 |- (ph -> (ps -> (ch -> th)))
Assertion
Ref Expression
imp3a |- (ph -> ((ps /\ ch) -> th))
Proof of Theorem imp3a
StepHypRef Expression
1 imp3.1 . 2 |- (ph -> (ps -> (ch -> th)))
2 impexp 347 . 2 |- (((ps /\ ch) -> th) <-> (ps -> (ch -> th)))
31, 2sylibr 200 1 |- (ph -> ((ps /\ ch) -> th))
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  imp32 363  imp4c 366  imp4d 367  adantld 390  imdistan 442  syland 457  dedlemb 761  3expib 834  sbied 1191  equs5 1216  a12study 1371  a12studyALT 1372  ra42 1688  r19.23ad 1737  reu3 1921  sbciegft 1949  uniiunlem 2122  prel12 2475  opthpr 2476  trel 2677  sotrieq 2852  elpwunsn 2902  wefrc 2933  tz7.7 2963  ordtr2 2992  oneqmini 3007  onmindif2 3051  peano5 3143  tfindsg2 3153  relop 3265  funssres 3538  fv3 3718  fopab2 3808  funfvima 3837  cbvfo 3870  isomin 3884  isofrlem 3886  f1oweALT 3891  tfrlem2 3897  tfr3 3911  tz7.48-1 3941  tz7.48-2 3942  tz7.49c 3945  omordi 4181  odi 4194  omass 4195  oen0 4197  oeordi 4198  nnmordi 4230  th3qlem1 4298  unen 4414  ensdomtr 4451  sdomen2 4462  ssenen 4484  pssnn 4513  domfi 4516  isfinite2 4523  unifi 4532  fiint 4534  fodomfib 4541  suplub 4555  supnub 4556  inf3lem2 4586  zfregs 4619  aceq6b 4714  zorn2lem7 4766  fodom 4770  brdom6disj 4777  unidom 4780  unxpdomlem 4815  ondomon 4828  alephord2i 4849  cardinfima 4863  alephval2 4874  indpi 5006  ltexpq 5052  ltrpq 5057  genpss 5079  genpnmax 5082  distrlem1pr 5099  distrlem5pr 5103  1idpr 5105  prlem934a 5109  ltaddpr 5112  ltexprlem1 5114  ltexprlem6 5119  prlem936b 5126  prlem936 5127  reclem4pr 5131  suplem1pr 5133  mulcmpblnr 5155  recexsrlem 5184  recexsr 5188  ltlent 5495  lelttrt 5496  ltletrt 5497  letrt 5498  xrlelttrt 5535  xrltletrt 5536  xrletrt 5537  mulgt1t 5801  nnleltp1t 5901  sup2 5998  supxrre 6030  zltp1let 6128  uzwo4OLD 6158  flval3t 6182  ser1add2 6275  ser1add 6276  elioc2t 6322  elico2t 6323  elicc2t 6324  uzwo 6387  uzwoOLD 6388  fsequb 6455  expgt0t 6520  expgt1t 6523  recexpt 6526  expword2it 6536  bernneq 6583  sqr2irrlem3 6656  creur 6673  creui 6674  cau4i 6855  cau5 6856  fsumcom 6966  fsumrev 6967  clim2serzt 7070  iserzmulc1 7072  caucvglem4 7096  cvgratlem1ALT 7182  cvgratlem1 7185  cvgratlem2 7186  abscncflem 7209  ivthlem7 7222  ivthlem7OLD 7231  acdc2 7432  acdc 7437  znnenlemOLD 7444  infpnlem1 7449  subtop 7588  clsval2 7627  neindisj 7672  sncld 7726  bl2in 7783  rnblssm 7791  metcnp 7826  metcnss 7837  lmuni 7886  lmle 7895  xpcn 7910  iscms2lem4 7926  lmcau 7930  bcthlem16 7948  bcthlem17 7949  bcthlem26 7958  grplactf1o 8034  ipblnfi 8447  ubthlem13 8472  spwmo 8580  ocin 9085  occllem6 9094  projlem26 9127  pjtheu 9150  shmods 9277  spansneleq 9409  spansneleqOLD 9410  spansncv 9514  nlelch 9909  cnlnssadj 9928  leopmulit 9978  pjnmop 9986  stjt 10072  mdsl0 10145  atom1d 10188  atcvat2 10222  irredlem1 10225  irred 10229  mdsymlem3 10240  mdsymlem6 10243  sumdmdi 10249  uninqs 10342  cdrci 10381  cmphmp 10408  hmphsyma 10415  hmphtr 10418  homcard 10426  qusp 10430
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain