MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim2d Structured version   Visualization version   Unicode version

Theorem imim2d 54
Description: Deduction adding nested antecedents. Deduction associated with imim2 55 and imim2i 16. (Contributed by NM, 10-Jan-1993.)
Hypothesis
Ref Expression
imim2d.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
imim2d  |-  ( ph  ->  ( ( th  ->  ps )  ->  ( th  ->  ch ) ) )

Proof of Theorem imim2d
StepHypRef Expression
1 imim2d.1 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
21a1d 26 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ch ) ) )
32a2d 29 1  |-  ( ph  ->  ( ( th  ->  ps )  ->  ( th  ->  ch ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim2  55  embantd  56  imim12d  77  anc2r  563  pm5.31  596  ornldOLD  915  dedlem0b  970  nic-ax  1567  nic-axALT  1568  19.23tOLD  2003  nfimd  2011  2eu6  2398  ssuni  4234  omordi  7293  nnawordi  7348  nnmordi  7358  omabs  7374  omsmolem  7380  alephordi  8531  dfac5  8585  dfac2a  8586  fin23lem14  8789  facdiv  12504  facwordi  12506  o1lo1  13650  rlimuni  13663  o1co  13699  rlimcn1  13701  rlimcn2  13703  rlimo1  13729  lo1add  13739  lo1mul  13740  rlimno1  13766  caucvgrlem  13785  caucvgrlemOLD  13786  caucvgrlem2  13789  gcdcllem1  14522  algcvgblem  14585  isprm5  14700  prmfac1  14720  infpnlem1  14903  gsummptnn0fz  17664  gsummoncoe1  18947  dmatscmcl  19577  decpmatmulsumfsupp  19846  pmatcollpw1lem1  19847  pmatcollpw2lem  19850  pmatcollpwfi  19855  pm2mpmhmlem1  19891  pm2mp  19898  cpmidpmatlem3  19945  cayhamlem4  19961  isclo2  20153  lmcls  20367  isnrm3  20424  dfcon2  20483  1stcrest  20517  dfac14lem  20681  cnpflf2  21064  isucn2  21343  cncfco  21988  ovolicc2lem3  22521  dyadmbllem  22606  itgcn  22849  aalioulem2  23338  aalioulem3  23339  ulmcn  23403  rlimcxp  23948  o1cxp  23949  chtppilimlem2  24361  chtppilim  24362  frgrancvvdgeq  25820  mdsymlem6  28110  crefss  28725  ss2mcls  30255  mclsax  30256  rdgprc  30490  bj-imim21  31207  bj-axtd  31222  bj-alrimh  31253  bj-ssbim  31279  bj-nfdt  31334  rdgeqoa  31818  pm5.31r  32472  pclclN  33501  isnacs3  35597  syl5imp  36913  imbi12VD  37310  sbcim2gVD  37312  pthdlem1  39792  ply1mulgsumlem3  40453  ply1mulgsumlem4  40454
  Copyright terms: Public domain W3C validator