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  1438  nic-axALT  1439  19.23t  1801  nfimd  1810  spimt  1979  ssuni  3930  omordi  6651  nnawordi  6706  nnmordi  6716  omabs  6732  omsmolem  6738  alephordi  7791  dfac5  7845  dfac2a  7846  fin23lem14  8049  facdiv  11393  facwordi  11395  o1lo1  12107  rlimuni  12120  o1co  12156  rlimcn1  12158  rlimcn2  12160  rlimo1  12186  lo1add  12196  lo1mul  12197  rlimno1  12223  caucvgrlem  12242  caucvgrlem2  12244  gcdcllem1  12787  algcvgblem  12844  isprm5  12888  prmfac1  12894  infpnlem1  13054  isclo2  16931  lmcls  17136  isnrm3  17193  dfcon2  17251  1stcrest  17285  dfac14lem  17417  cnpflf2  17797  cncfco  18514  ovolicc2lem3  18982  dyadmbllem  19058  itgcn  19301  aalioulem2  19817  aalioulem3  19818  ulmcn  19882  rlimcxp  20379  o1cxp  20380  chtppilimlem2  20735  chtppilim  20736  mdsymlem6  23102  rdgprc  24709  wl-adnestantdALTOLD  25468  wl-bitr1  25469  pm5.31r  26040  isnacs3  26108  frgrancvvdgeq  27876  syl5imp  28019  imbi12VD  28411  sbcim2gVD  28413  spimtNEW7  28930  pclclN  30149
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator