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

Theorem imim2d 52
Description: Deduction adding nested antecedents. (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 25 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ch ) ) )
32a2d 26 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  53  embantd  54  imim12d  74  anc2r  556  pm5.31  588  ornldOLD  897  dedlem0b  951  nic-ax  1490  nic-axALT  1491  19.23t  1856  nfimd  1864  2eu6  2393  ssuni  4267  omordi  7215  nnawordi  7270  nnmordi  7280  omabs  7296  omsmolem  7302  alephordi  8455  dfac5  8509  dfac2a  8510  fin23lem14  8713  facdiv  12333  facwordi  12335  o1lo1  13323  rlimuni  13336  o1co  13372  rlimcn1  13374  rlimcn2  13376  rlimo1  13402  lo1add  13412  lo1mul  13413  rlimno1  13439  caucvgrlem  13458  caucvgrlem2  13460  gcdcllem1  14008  algcvgblem  14065  isprm5  14112  prmfac1  14118  infpnlem1  14287  gsummptnn0fz  16817  gsummoncoe1  18145  dmatscmcl  18800  decpmatmulsumfsupp  19069  pmatcollpw1lem1  19070  pmatcollpw2lem  19073  pmatcollpwfi  19078  pm2mpmhmlem1  19114  pm2mp  19121  cpmidpmatlem3  19168  cayhamlem4  19184  isclo2  19383  lmcls  19597  isnrm3  19654  dfcon2  19714  1stcrest  19748  dfac14lem  19881  cnpflf2  20264  isucn2  20545  cncfco  21174  ovolicc2lem3  21693  dyadmbllem  21771  itgcn  22012  aalioulem2  22491  aalioulem3  22492  ulmcn  22556  rlimcxp  23059  o1cxp  23060  chtppilimlem2  23415  chtppilim  23416  frgrancvvdgeq  24748  mdsymlem6  27031  rdgprc  28832  pm5.31r  30226  isnacs3  30274  ply1mulgsumlem3  32087  ply1mulgsumlem4  32088  syl5imp  32379  imbi12VD  32771  sbcim2gVD  32773  bj-axtd  33282  bj-alrimh  33314  bj-nfdt  33349  pclclN  34705
  Copyright terms: Public domain W3C validator