MPE Home 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  759  ad4ant23OLD  763  ad4ant124OLD  1217  merco2  1832  equvel  2461  propeqop  5161  funopsn  6639  xpexr  7339  omordi  7884  omwordi  7889  odi  7897  omass  7898  oen0  7904  oewordi  7909  oewordri  7910  nnmwordi  7953  omabs  7965  fisupg  8448  fiinfg  8645  cantnfle  8816  cantnflem1  8834  pr2ne  9112  gchina  9807  nqereu  10037  supsrlem  10218  1re  10326  lemul1a  11167  nnsub  11353  xlemul1a  12363  xrsupsslem  12382  xrinfmsslem  12383  xrub  12387  supxrunb1  12394  supxrunb2  12395  difelfzle  12703  addmodlteq  12996  seqcl2  13069  facdiv  13323  facwordi  13325  faclbnd  13326  swrdswrdlem  13743  pfxccat3  13793  swrdccat3OLD  13794  dvdsabseq  15370  divgcdcoprm0  15709  exprmfct  15745  prmfac1  15760  pockthg  15939  cply1mul  19982  mdetralt  20736  cmpsub  21528  fbfinnfr  21969  alexsubALTlem2  22176  alexsubALTlem3  22177  ovolicc2lem3  23623  fta1g  24264  fta1  24400  mulcxp  24768  cxpcn3lem  24828  gausslemma2dlem4  25442  colinearalg  26138  upgrwlkdvdelem  26981  umgr2wlk  27229  clwwlknwwlksn  27336  clwwlknwwlksnOLD  27337  clwwlknonex2lem2  27439  dmdbr5ati  29797  cvmlift3lem4  31812  dfon2lem9  32199  fscgr  32691  colinbtwnle  32729  broutsideof2  32733  a1i14  32798  a1i24  32799  ordcmp  32945  wl-aleq  33803  itg2addnc  33943  filbcmb  34014  mpt2bi123f  34448  mptbi12f  34452  ac6s6  34457  ltrnid  36147  cdleme25dN  36368  ntrneiiso  39158  ee323  39481  vd13  39583  vd23  39584  ee03  39724  ee23an  39740  ee32  39742  ee32an  39744  ee123  39746  iccpartgt  42190  stgoldbwt  42433  tgoldbach  42474  nzerooringczr  42858
  Copyright terms: Public domain W3C validator