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

Theorem imim2d 52
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  53  embantd  54  imim12d  74  anc2r  556  pm5.31  588  ornldOLD  899  dedlem0b  953  nic-ax  1506  nic-axALT  1507  19.23t  1910  nfimd  1918  2eu6  2383  ssuni  4273  omordi  7233  nnawordi  7288  nnmordi  7298  omabs  7314  omsmolem  7320  alephordi  8472  dfac5  8526  dfac2a  8527  fin23lem14  8730  facdiv  12368  facwordi  12370  o1lo1  13372  rlimuni  13385  o1co  13421  rlimcn1  13423  rlimcn2  13425  rlimo1  13451  lo1add  13461  lo1mul  13462  rlimno1  13488  caucvgrlem  13507  caucvgrlem2  13509  gcdcllem1  14161  algcvgblem  14218  isprm5  14265  prmfac1  14271  infpnlem1  14440  gsummptnn0fz  17141  gsummoncoe1  18473  dmatscmcl  19132  decpmatmulsumfsupp  19401  pmatcollpw1lem1  19402  pmatcollpw2lem  19405  pmatcollpwfi  19410  pm2mpmhmlem1  19446  pm2mp  19453  cpmidpmatlem3  19500  cayhamlem4  19516  isclo2  19716  lmcls  19930  isnrm3  19987  dfcon2  20046  1stcrest  20080  dfac14lem  20244  cnpflf2  20627  isucn2  20908  cncfco  21537  ovolicc2lem3  22056  dyadmbllem  22134  itgcn  22375  aalioulem2  22855  aalioulem3  22856  ulmcn  22920  rlimcxp  23429  o1cxp  23430  chtppilimlem2  23785  chtppilim  23786  frgrancvvdgeq  25170  mdsymlem6  27454  crefss  28013  ss2mcls  29125  mclsax  29126  rdgprc  29444  pm5.31r  30799  isnacs3  30847  ply1mulgsumlem3  33132  ply1mulgsumlem4  33133  syl5imp  33425  imbi12VD  33816  sbcim2gVD  33818  bj-axtd  34325  bj-alrimh  34351  bj-nfdt  34392  pclclN  35758
  Copyright terms: Public domain W3C validator