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, 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  52  embantd  53  imim12d  74  anc2r  554  pm5.31  586  ornldOLD  900  dedlem0b  954  nic-ax  1526  nic-axALT  1527  19.23t  1937  nfimd  1945  2eu6  2334  ssuni  4213  omordi  7252  nnawordi  7307  nnmordi  7317  omabs  7333  omsmolem  7339  alephordi  8487  dfac5  8541  dfac2a  8542  fin23lem14  8745  facdiv  12409  facwordi  12411  o1lo1  13509  rlimuni  13522  o1co  13558  rlimcn1  13560  rlimcn2  13562  rlimo1  13588  lo1add  13598  lo1mul  13599  rlimno1  13625  caucvgrlem  13644  caucvgrlem2  13646  gcdcllem1  14358  algcvgblem  14415  isprm5  14462  prmfac1  14468  infpnlem1  14637  gsummptnn0fz  17334  gsummoncoe1  18666  dmatscmcl  19297  decpmatmulsumfsupp  19566  pmatcollpw1lem1  19567  pmatcollpw2lem  19570  pmatcollpwfi  19575  pm2mpmhmlem1  19611  pm2mp  19618  cpmidpmatlem3  19665  cayhamlem4  19681  isclo2  19882  lmcls  20096  isnrm3  20153  dfcon2  20212  1stcrest  20246  dfac14lem  20410  cnpflf2  20793  isucn2  21074  cncfco  21703  ovolicc2lem3  22222  dyadmbllem  22300  itgcn  22541  aalioulem2  23021  aalioulem3  23022  ulmcn  23086  rlimcxp  23629  o1cxp  23630  chtppilimlem2  24040  chtppilim  24041  frgrancvvdgeq  25460  mdsymlem6  27740  crefss  28305  ss2mcls  29780  mclsax  29781  rdgprc  30014  bj-axtd  30746  bj-alrimh  30772  bj-nfdt  30813  pm5.31r  31876  pclclN  32908  isnacs3  35004  syl5imp  36299  imbi12VD  36704  sbcim2gVD  36706  ply1mulgsumlem3  38499  ply1mulgsumlem4  38500
  Copyright terms: Public domain W3C validator