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  1553  equveli  2061  sotriOLD  5398  xpexr  6724  omordi  7215  omwordi  7220  odi  7228  omass  7229  oen0  7235  oewordi  7240  oewordri  7241  nnmwordi  7284  omabs  7296  fisupg  7767  cantnfle  8089  cantnflem1  8107  cantnfleOLD  8119  cantnflem1OLD  8130  pr2ne  8382  axpowndlem3OLD  8975  gchina  9076  nqereu  9306  supsrlem  9487  1re  9594  lemul1a  10395  nnsub  10573  xlemul1a  11479  xrsupsslem  11497  xrinfmsslem  11498  xrub  11502  supxrunb1  11510  supxrunb2  11511  difelfzle  11784  fsuppmapnn0fiubex  12065  seqcl2  12092  facdiv  12332  facwordi  12334  faclbnd  12335  swrdswrdlem  12646  swrdccat3  12679  exprmfct  14109  prmfac1  14117  pockthg  14282  cply1mul  18122  mdetralt  18893  cmpsub  19682  fbfinnfr  20093  alexsubALTlem2  20299  alexsubALTlem3  20300  ovolicc2lem3  21681  fta1g  22319  fta1  22454  mulcxp  22810  cxpcn3lem  22865  colinearalg  23905  vdn0frgrav2  24716  vdgn0frgrav2  24717  2spotmdisj  24761  numclwwlkovf2ex  24779  dmdbr5ati  27033  cvmlift3lem4  28423  dfon2lem9  28816  fscgr  29323  colinbtwnle  29361  broutsideof2  29365  ordcmp  29505  wl-aleq  29581  itg2addnc  29662  a1i14  29708  a1i24  29709  a1i34  29710  filbcmb  29850  mpt2bi123f  30191  mptbi12f  30195  ac6s6  30200  usgfis  31929  ad4ant124  32315  ee323  32365  vd13  32476  vd23  32477  ee03  32627  ee23an  32643  ee32  32645  ee32an  32647  ee123  32649  ltrnid  34940  cdleme25dN  35161
  Copyright terms: Public domain W3C validator