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

Theorem imim2d 54
Description: Deduction adding nested antecedents. Deduction associated with imim2 55 and imim2i 16. (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 26 . 2  |-  ( ph  ->  ( th  ->  ( ps  ->  ch ) ) )
32a2d 29 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  55  embantd  56  imim12d  77  anc2r  558  pm5.31  590  ornldOLD  907  dedlem0b  961  nic-ax  1552  nic-axALT  1553  19.23tOLD  1965  nfimd  1973  2eu6  2356  ssuni  4238  omordi  7272  nnawordi  7327  nnmordi  7337  omabs  7353  omsmolem  7359  alephordi  8506  dfac5  8560  dfac2a  8561  fin23lem14  8764  facdiv  12472  facwordi  12474  o1lo1  13589  rlimuni  13602  o1co  13638  rlimcn1  13640  rlimcn2  13642  rlimo1  13668  lo1add  13678  lo1mul  13679  rlimno1  13705  caucvgrlem  13724  caucvgrlemOLD  13725  caucvgrlem2  13728  gcdcllem1  14461  algcvgblem  14524  isprm5  14639  prmfac1  14659  infpnlem1  14842  gsummptnn0fz  17603  gsummoncoe1  18886  dmatscmcl  19515  decpmatmulsumfsupp  19784  pmatcollpw1lem1  19785  pmatcollpw2lem  19788  pmatcollpwfi  19793  pm2mpmhmlem1  19829  pm2mp  19836  cpmidpmatlem3  19883  cayhamlem4  19899  isclo2  20091  lmcls  20305  isnrm3  20362  dfcon2  20421  1stcrest  20455  dfac14lem  20619  cnpflf2  21002  isucn2  21281  cncfco  21926  ovolicc2lem3  22459  dyadmbllem  22544  itgcn  22787  aalioulem2  23276  aalioulem3  23277  ulmcn  23341  rlimcxp  23886  o1cxp  23887  chtppilimlem2  24299  chtppilim  24300  frgrancvvdgeq  25757  mdsymlem6  28047  crefss  28672  ss2mcls  30202  mclsax  30203  rdgprc  30436  bj-axtd  31169  bj-alrimh  31195  bj-nfdt  31237  pm5.31r  32343  pclclN  33375  isnacs3  35471  syl5imp  36727  imbi12VD  37131  sbcim2gVD  37133  ply1mulgsumlem3  39454  ply1mulgsumlem4  39455
  Copyright terms: Public domain W3C validator