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

Theorem imim2d 48
Description: Deduction adding nested antecedents. (Contributed by NM, 5-Aug-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 22 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ch ) ) )
32a2d 23 1  |-  ( ph  ->  ( ( th  ->  ps )  ->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim2  49  embantd  50  imim12d  68  anc2r  539  pm5.31  571  dedlem0b  919  nic-ax  1428  nic-axALT  1429  spimt  1914  ssuni  3849  omordi  6564  nnawordi  6619  nnmordi  6629  omabs  6645  omsmolem  6651  alephordi  7701  dfac5  7755  dfac2a  7756  fin23lem14  7959  facdiv  11300  facwordi  11302  o1lo1  12011  rlimuni  12024  o1co  12060  rlimcn1  12062  rlimcn2  12064  rlimo1  12090  lo1add  12100  lo1mul  12101  rlimno1  12127  caucvgrlem  12145  caucvgrlem2  12147  gcdcllem1  12690  algcvgblem  12747  isprm5  12791  prmfac1  12797  infpnlem1  12957  isclo2  16825  lmcls  17030  isnrm3  17087  dfcon2  17145  1stcrest  17179  dfac14lem  17311  cnpflf2  17695  cncfco  18411  ovolicc2lem3  18878  dyadmbllem  18954  itgcn  19197  aalioulem2  19713  aalioulem3  19714  ulmcn  19776  rlimcxp  20268  o1cxp  20269  chtppilimlem2  20623  chtppilim  20624  mdsymlem6  22988  rdgprc  24151  wl-adnestantdALTOLD  24909  wl-bitr1  24910  pm5.31r  26717  isnacs3  26785  syl5imp  28274  imbi12VD  28649  sbcim2gVD  28651  pclclN  30080
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator