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

Theorem a1dd 44
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 31 1  |-  ( ph  ->  ( ps  ->  ( th  ->  ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  merco2  1510  nfsb4tOLD  2128  sotriOLD  5266  xpexr  5307  omordi  6809  omwordi  6814  odi  6822  omass  6823  oen0  6829  oewordi  6834  oewordri  6835  nnmwordi  6878  omabs  6890  fisupg  7355  cantnfle  7626  cantnflem1  7645  pr2ne  7889  axpowndlem3  8474  gchina  8574  nqereu  8806  supsrlem  8986  1re  9090  lemul1a  9864  nnsub  10038  xlemul1a  10867  xrsupsslem  10885  xrinfmsslem  10886  xrub  10890  supxrunb1  10898  supxrunb2  10899  seqcl2  11341  facdiv  11578  facwordi  11580  faclbnd  11581  exprmfct  13110  prmfac1  13118  pockthg  13274  cmpsub  17463  fbfinnfr  17873  alexsubALTlem2  18079  alexsubALTlem3  18080  ovolicc2lem3  19415  fta1g  20090  fta1  20225  mulcxp  20576  cxpcn3lem  20631  dmdbr5ati  23925  cvmlift3lem4  25009  dfon2lem9  25418  colinearalg  25849  fscgr  26014  colinbtwnle  26052  broutsideof2  26056  ordcmp  26197  wl-aleq  26235  itg2addnc  26259  a1i14  26300  a1i24  26301  a1i34  26302  filbcmb  26442  swrdswrdlem  28198  swrdccat3  28215  vdn0frgrav2  28414  vdgn0frgrav2  28415  2spotmdisj  28457  ad4ant124  28541  ee323  28590  vd13  28702  vd23  28703  ee03  28853  ee23an  28869  ee32  28871  ee32an  28873  ee123  28875  nfsb4twAUX7  29576  nfsb4tOLD7  29745  nfsb4tw2AUXOLD7  29746  ltrnid  30932  cdleme25dN  31153
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 8
  Copyright terms: Public domain W3C validator