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

Theorem a1dd 46
Description: Deduction introducing a nested embedded antecedent. (Contributed by NM, 17-Dec-2004.) (Proof shortened by Mel L. 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 6 . 2  |-  ( ch 
->  ( th  ->  ch ) )
31, 2syl6 33 1  |-  ( ph  ->  ( 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:  merco2  1543  equveli  2038  sotriOLD  5242  xpexr  6530  omordi  7017  omwordi  7022  odi  7030  omass  7031  oen0  7037  oewordi  7042  oewordri  7043  nnmwordi  7086  omabs  7098  fisupg  7572  cantnfle  7891  cantnflem1  7909  cantnfleOLD  7921  cantnflem1OLD  7932  pr2ne  8184  axpowndlem3OLD  8777  gchina  8878  nqereu  9110  supsrlem  9290  1re  9397  lemul1a  10195  nnsub  10372  xlemul1a  11263  xrsupsslem  11281  xrinfmsslem  11282  xrub  11286  supxrunb1  11294  supxrunb2  11295  seqcl2  11836  facdiv  12075  facwordi  12077  faclbnd  12078  swrdswrdlem  12365  swrdccat3  12395  exprmfct  13808  prmfac1  13816  pockthg  13979  mdetralt  18426  cmpsub  19015  fbfinnfr  19426  alexsubALTlem2  19632  alexsubALTlem3  19633  ovolicc2lem3  21014  fta1g  21651  fta1  21786  mulcxp  22142  cxpcn3lem  22197  colinearalg  23168  dmdbr5ati  25838  cvmlift3lem4  27223  dfon2lem9  27616  fscgr  28123  colinbtwnle  28161  broutsideof2  28165  ordcmp  28305  wl-aleq  28376  itg2addnc  28458  a1i14  28504  a1i24  28505  a1i34  28506  filbcmb  28646  mpt2bi123f  28987  mptbi12f  28991  ac6s6  28996  difelfzle  30499  vdn0frgrav2  30628  vdgn0frgrav2  30629  2spotmdisj  30673  numclwwlkovf2ex  30691  fsuppmapnn0fiubex  30812  ad4ant124  31174  ee323  31224  vd13  31335  vd23  31336  ee03  31486  ee23an  31502  ee32  31504  ee32an  31506  ee123  31508  ltrnid  33791  cdleme25dN  34012
  Copyright terms: Public domain W3C validator