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  1655  nfsb4t  2020  sotriOLD  5075  xpexr  5114  omordi  6564  omwordi  6569  odi  6577  omass  6578  oen0  6584  oewordi  6589  oewordri  6590  nnmwordi  6633  omabs  6645  fisupg  7105  cantnfle  7372  cantnflem1  7391  pr2ne  7635  axpowndlem3  8221  gchina  8321  nqereu  8553  supsrlem  8733  1re  8837  lemul1a  9610  nnsub  9784  xlemul1a  10608  xrsupsslem  10625  xrinfmsslem  10626  xrub  10630  supxrunb1  10638  supxrunb2  10639  seqcl2  11064  facdiv  11300  facwordi  11302  faclbnd  11303  exprmfct  12789  prmfac1  12797  pockthg  12953  cmpsub  17127  fbfinnfr  17536  alexsubALTlem2  17742  alexsubALTlem3  17743  ovolicc2lem3  18878  fta1g  19553  fta1  19688  mulcxp  20032  cxpcn3lem  20087  dmdbr5ati  23002  cvmlift3lem4  23853  dfon2lem9  24147  colinearalg  24538  fscgr  24703  colinbtwnle  24741  broutsideof2  24745  ordcmp  24886  untind  25018  multinv  25422  truni3  25507  fnmulcv  25684  distsava  25689  intvconlem1  25703  hdrmp  25706  cmpassoh  25801  lemindclsbu  25995  gltpntl  26072  a1i14  26202  a1i24  26203  a1i34  26204  filbcmb  26432  ee323  28269  vd13  28373  vd23  28374  ee03  28516  ee23an  28532  ee32  28534  ee32an  28536  ee123  28538  a12study6  29118  a12stdy4  29129  ltrnid  30324  cdleme25dN  30545
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator