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

Theorem imim2d 51
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 24 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ch ) ) )
32a2d 25 1  |-  ( ph  ->  ( ( th  ->  ps )  ->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim2  52  embantd  53  imim12d  71  anc2r  541  pm5.31  573  dedlem0b  921  nic-ax  1448  nic-axALT  1449  19.23t  1819  nfimd  1828  spimtOLD  1957  ssuni  4039  omordi  6812  nnawordi  6867  nnmordi  6877  omabs  6893  omsmolem  6899  alephordi  7960  dfac5  8014  dfac2a  8015  fin23lem14  8218  facdiv  11583  facwordi  11585  o1lo1  12336  rlimuni  12349  o1co  12385  rlimcn1  12387  rlimcn2  12389  rlimo1  12415  lo1add  12425  lo1mul  12426  rlimno1  12452  caucvgrlem  12471  caucvgrlem2  12473  gcdcllem1  13016  algcvgblem  13073  isprm5  13117  prmfac1  13123  infpnlem1  13283  isclo2  17157  lmcls  17371  isnrm3  17428  dfcon2  17487  1stcrest  17521  dfac14lem  17654  cnpflf2  18037  isucn2  18314  cncfco  18942  ovolicc2lem3  19420  dyadmbllem  19496  itgcn  19737  aalioulem2  20255  aalioulem3  20256  ulmcn  20320  rlimcxp  20817  o1cxp  20818  chtppilimlem2  21173  chtppilim  21174  mdsymlem6  23916  rdgprc  25427  wl-bitr1  26225  pm5.31r  26714  isnacs3  26778  frgrancvvdgeq  28506  syl5imp  28669  imbi12VD  29059  sbcim2gVD  29061  spimtNEW7  29581  pclclN  30762
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
  Copyright terms: Public domain W3C validator