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  ad4ant124OLD  1161  ad4ant13OLD  1184  ad4ant23OLD  1188  merco2  1798  equvel  2472  propeqop  5106  funopsn  6564  xpexr  7259  omordi  7803  omwordi  7808  odi  7816  omass  7817  oen0  7823  oewordi  7828  oewordri  7829  nnmwordi  7872  omabs  7884  fisupg  8361  fiinfg  8558  cantnfle  8729  cantnflem1  8747  pr2ne  8989  gchina  9684  nqereu  9914  supsrlem  10095  1re  10202  lemul1a  11040  nnsub  11222  xlemul1a  12282  xrsupsslem  12301  xrinfmsslem  12302  xrub  12306  supxrunb1  12313  supxrunb2  12314  difelfzle  12617  addmodlteq  12910  seqcl2  12984  facdiv  13239  facwordi  13241  faclbnd  13242  swrdswrdlem  13630  swrdccat3  13663  dvdsabseq  15208  divgcdcoprm0  15552  exprmfct  15589  prmfac1  15604  pockthg  15783  cply1mul  19837  mdetralt  20587  cmpsub  21376  fbfinnfr  21817  alexsubALTlem2  22024  alexsubALTlem3  22025  ovolicc2lem3  23458  fta1g  24097  fta1  24233  mulcxp  24601  cxpcn3lem  24658  gausslemma2dlem4  25264  colinearalg  25960  upgrwlkdvdelem  26813  umgr2wlk  27040  clwwlknwwlksn  27137  clwwlknwwlksnOLD  27138  clwwlknonex2lem2  27228  dmdbr5ati  29561  cvmlift3lem4  31582  dfon2lem9  31972  fscgr  32464  colinbtwnle  32502  broutsideof2  32506  a1i14  32571  a1i24  32572  ordcmp  32723  wl-aleq  33604  itg2addnc  33746  filbcmb  33817  mpt2bi123f  34253  mptbi12f  34257  ac6s6  34262  ltrnid  35893  cdleme25dN  36115  ntrneiiso  38860  ee323  39185  vd13  39297  vd23  39298  ee03  39439  ee23an  39455  ee32  39457  ee32an  39459  ee123  39461  iccpartgt  41842  pfxccat3  41905  stgoldbwt  42143  tgoldbach  42184  tgoldbachOLD  42191  nzerooringczr  42551
 Copyright terms: Public domain W3C validator