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

Theorem imim2d 50
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 23 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ch ) ) )
32a2d 24 1  |-  ( ph  ->  ( ( th  ->  ps )  ->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  imim2  51  embantd  52  imim12d  70  anc2r  540  pm5.31  572  dedlem0b  920  nic-ax  1444  nic-axALT  1445  19.23t  1814  nfimd  1823  spimtOLD  1954  ssuni  3997  omordi  6768  nnawordi  6823  nnmordi  6833  omabs  6849  omsmolem  6855  alephordi  7911  dfac5  7965  dfac2a  7966  fin23lem14  8169  facdiv  11533  facwordi  11535  o1lo1  12286  rlimuni  12299  o1co  12335  rlimcn1  12337  rlimcn2  12339  rlimo1  12365  lo1add  12375  lo1mul  12376  rlimno1  12402  caucvgrlem  12421  caucvgrlem2  12423  gcdcllem1  12966  algcvgblem  13023  isprm5  13067  prmfac1  13073  infpnlem1  13233  isclo2  17107  lmcls  17320  isnrm3  17377  dfcon2  17435  1stcrest  17469  dfac14lem  17602  cnpflf2  17985  isucn2  18262  cncfco  18890  ovolicc2lem3  19368  dyadmbllem  19444  itgcn  19687  aalioulem2  20203  aalioulem3  20204  ulmcn  20268  rlimcxp  20765  o1cxp  20766  chtppilimlem2  21121  chtppilim  21122  mdsymlem6  23864  rdgprc  25365  wl-bitr1  26124  pm5.31r  26590  isnacs3  26654  frgrancvvdgeq  28146  syl5imp  28306  imbi12VD  28694  sbcim2gVD  28696  spimtNEW7  29213  pclclN  30373
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator