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

Theorem a1dd 42
Description: Deduction introducing a nested embedded antecedent. (Contributed by NM, 17-Dec-2004.) (Proof shortened by O'Cat, 15-Jan-2008.)
Hypothesis
Ref Expression
a1dd.1  |-  ( ph  ->  ( ps  ->  ch ) )
Assertion
Ref Expression
a1dd  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )

Proof of Theorem a1dd
StepHypRef Expression
1 a1dd.1 . 2  |-  ( ph  ->  ( ps  ->  ch ) )
2 ax-1 5 . 2  |-  ( ch 
->  ( th  ->  ch ) )
31, 2syl6 29 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  merco2  1491  ax12b  1674  nfsb4t  2033  sotriOLD  5091  xpexr  5130  omordi  6580  omwordi  6585  odi  6593  omass  6594  oen0  6600  oewordi  6605  oewordri  6606  nnmwordi  6649  omabs  6661  fisupg  7121  cantnfle  7388  cantnflem1  7407  pr2ne  7651  axpowndlem3  8237  gchina  8337  nqereu  8569  supsrlem  8749  1re  8853  lemul1a  9626  nnsub  9800  xlemul1a  10624  xrsupsslem  10641  xrinfmsslem  10642  xrub  10646  supxrunb1  10654  supxrunb2  10655  seqcl2  11080  facdiv  11316  facwordi  11318  faclbnd  11319  exprmfct  12805  prmfac1  12813  pockthg  12969  cmpsub  17143  fbfinnfr  17552  alexsubALTlem2  17758  alexsubALTlem3  17759  ovolicc2lem3  18894  fta1g  19569  fta1  19704  mulcxp  20048  cxpcn3lem  20103  dmdbr5ati  23018  cvmlift3lem4  23868  dfon2lem9  24218  colinearalg  24610  fscgr  24775  colinbtwnle  24813  broutsideof2  24817  ordcmp  24958  itg2addnc  25005  untind  25121  multinv  25525  truni3  25610  fnmulcv  25787  distsava  25792  intvconlem1  25806  hdrmp  25809  cmpassoh  25904  lemindclsbu  26098  gltpntl  26175  a1i14  26305  a1i24  26306  a1i34  26307  filbcmb  26535  ad4ant124  28522  ee323  28568  vd13  28678  vd23  28679  ee03  28830  ee23an  28846  ee32  28848  ee32an  28850  ee123  28852  nfsb4twAUX7  29551  nfsb4tOLD7  29699  nfsb4tw2AUXOLD7  29700  a12study6  29740  a12stdy4  29751  ltrnid  30946  cdleme25dN  31167
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator