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  dedlem0b  944  nic-ax  1480  nic-axALT  1481  19.23t  1842  nfimd  1850  2eu6  2370  ssuni  4111  omordi  7003  nnawordi  7058  nnmordi  7068  omabs  7084  omsmolem  7090  alephordi  8242  dfac5  8296  dfac2a  8297  fin23lem14  8500  facdiv  12061  facwordi  12063  o1lo1  13013  rlimuni  13026  o1co  13062  rlimcn1  13064  rlimcn2  13066  rlimo1  13092  lo1add  13102  lo1mul  13103  rlimno1  13129  caucvgrlem  13148  caucvgrlem2  13150  gcdcllem1  13693  algcvgblem  13750  isprm5  13796  prmfac1  13802  infpnlem1  13969  isclo2  18690  lmcls  18904  isnrm3  18961  dfcon2  19021  1stcrest  19055  dfac14lem  19188  cnpflf2  19571  isucn2  19852  cncfco  20481  ovolicc2lem3  21000  dyadmbllem  21077  itgcn  21318  aalioulem2  21797  aalioulem3  21798  ulmcn  21862  rlimcxp  22365  o1cxp  22366  chtppilimlem2  22721  chtppilim  22722  mdsymlem6  25810  rdgprc  27606  pm5.31r  28995  isnacs3  29043  ornld  30111  frgrancvvdgeq  30633  gsummptnn0fz  30803  gsummoncoe1  30840  ply1mulgsumlem3  30843  ply1mulgsumlem4  30844  pmatcollpw2lem  30902  pmattomply1mhmlem0  30924  pmattomply1mhmlem1  30925  syl5imp  31214  imbi12VD  31606  sbcim2gVD  31608  bj-axtd  32126  bj-alrimh  32147  bj-nfdt  32182  pclclN  33532
  Copyright terms: Public domain W3C validator