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

Theorem a1dd 50
 Description: Double deduction introducing an antecedent. Deduction associated with a1d 25. Double deduction associated with ax-1 6 and a1i 11. (Contributed by NM, 17-Dec-2004.) (Proof shortened by Mel L. O'Cat, 15-Jan-2008.)
Hypothesis
Ref Expression
a1dd.1 (𝜑 → (𝜓𝜒))
Assertion
Ref Expression
a1dd (𝜑 → (𝜓 → (𝜃𝜒)))

Proof of Theorem a1dd
StepHypRef Expression
1 a1dd.1 . 2 (𝜑 → (𝜓𝜒))
2 ax-1 6 . 2 (𝜒 → (𝜃𝜒))
31, 2syl6 35 1 (𝜑 → (𝜓 → (𝜃𝜒)))
 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:  2a1dd  51  ad4ant13OLD  1316  ad4ant124OLD  1322  ad4ant23OLD  1326  merco2  1701  equvel  2375  propeqop  4999  funopsn  6453  xpexr  7148  omordi  7691  omwordi  7696  odi  7704  omass  7705  oen0  7711  oewordi  7716  oewordri  7717  nnmwordi  7760  omabs  7772  fisupg  8249  fiinfg  8446  cantnfle  8606  cantnflem1  8624  pr2ne  8866  gchina  9559  nqereu  9789  supsrlem  9970  1re  10077  lemul1a  10915  nnsub  11097  xlemul1a  12156  xrsupsslem  12175  xrinfmsslem  12176  xrub  12180  supxrunb1  12187  supxrunb2  12188  difelfzle  12491  addmodlteq  12785  seqcl2  12859  facdiv  13114  facwordi  13116  faclbnd  13117  swrdswrdlem  13505  swrdccat3  13538  dvdsabseq  15082  divgcdcoprm0  15426  exprmfct  15463  prmfac1  15478  pockthg  15657  cply1mul  19712  mdetralt  20462  cmpsub  21251  fbfinnfr  21692  alexsubALTlem2  21899  alexsubALTlem3  21900  ovolicc2lem3  23333  fta1g  23972  fta1  24108  mulcxp  24476  cxpcn3lem  24533  gausslemma2dlem4  25139  colinearalg  25835  upgrwlkdvdelem  26688  umgr2wlk  26914  clwwlknwwlksn  27000  clwwlknwwlksnOLD  27001  clwwlknonex2lem2  27083  2clwwlk2clwwlklem2lem2  27329  dmdbr5ati  29409  cvmlift3lem4  31430  dfon2lem9  31820  fscgr  32312  colinbtwnle  32350  broutsideof2  32354  a1i14  32419  a1i24  32420  ordcmp  32571  wl-aleq  33452  itg2addnc  33594  filbcmb  33665  mpt2bi123f  34101  mptbi12f  34105  ac6s6  34110  ltrnid  35739  cdleme25dN  35961  ntrneiiso  38706  ee323  39031  vd13  39143  vd23  39144  ee03  39285  ee23an  39301  ee32  39303  ee32an  39305  ee123  39307  iccpartgt  41688  pfxccat3  41751  stgoldbwt  41989  tgoldbach  42030  tgoldbachOLD  42037  nzerooringczr  42397
 Copyright terms: Public domain W3C validator