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 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  1548  equveli  2043  sotriOLD  5227  xpexr  6517  omordi  7001  omwordi  7006  odi  7014  omass  7015  oen0  7021  oewordi  7026  oewordri  7027  nnmwordi  7070  omabs  7082  fisupg  7556  cantnfle  7875  cantnflem1  7893  cantnfleOLD  7905  cantnflem1OLD  7916  pr2ne  8168  axpowndlem3OLD  8761  gchina  8862  nqereu  9094  supsrlem  9274  1re  9381  lemul1a  10179  nnsub  10356  xlemul1a  11247  xrsupsslem  11265  xrinfmsslem  11266  xrub  11270  supxrunb1  11278  supxrunb2  11279  seqcl2  11820  facdiv  12059  facwordi  12061  faclbnd  12062  swrdswrdlem  12349  swrdccat3  12379  exprmfct  13792  prmfac1  13800  pockthg  13963  mdetralt  18314  cmpsub  18903  fbfinnfr  19314  alexsubALTlem2  19520  alexsubALTlem3  19521  ovolicc2lem3  20902  fta1g  21582  fta1  21717  mulcxp  22073  cxpcn3lem  22128  colinearalg  23075  dmdbr5ati  25745  cvmlift3lem4  27125  dfon2lem9  27517  fscgr  28024  colinbtwnle  28062  broutsideof2  28066  ordcmp  28207  wl-aleq  28277  itg2addnc  28355  a1i14  28401  a1i24  28402  a1i34  28403  filbcmb  28543  mpt2bi123f  28884  mptbi12f  28888  ac6s6  28893  difelfzle  30396  vdn0frgrav2  30525  vdgn0frgrav2  30526  2spotmdisj  30570  numclwwlkovf2ex  30588  ad4ant124  30978  ee323  31028  vd13  31140  vd23  31141  ee03  31291  ee23an  31307  ee32  31309  ee32an  31311  ee123  31313  ltrnid  33467  cdleme25dN  33688
  Copyright terms: Public domain W3C validator