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  merco2  1730  equvel  2476  propeqop  5394  funopsn  6906  xpexr  7611  omordi  8182  omwordi  8187  odi  8195  omass  8196  oen0  8202  oewordi  8207  oewordri  8208  nnmwordi  8251  omabs  8264  fisupg  8755  fiinfg  8952  cantnfle  9123  cantnflem1  9141  pr2ne  9420  gchina  10110  nqereu  10340  supsrlem  10522  1re  10630  lemul1a  11483  xlemul1a  12671  xrsupsslem  12690  xrinfmsslem  12691  xrub  12695  supxrunb1  12702  supxrunb2  12703  difelfzle  13010  addmodlteq  13304  seqcl2  13378  facdiv  13637  facwordi  13639  faclbnd  13640  pfxccat3  14086  dvdsabseq  15653  divgcdcoprm0  15999  2mulprm  16027  exprmfct  16038  prmfac1  16053  pockthg  16232  cply1mul  20381  mdetralt  21136  cmpsub  21927  fbfinnfr  22368  alexsubALTlem2  22575  alexsubALTlem3  22576  ovolicc2lem3  24038  fta1g  24679  fta1  24815  mulcxp  25184  cxpcn3lem  25244  gausslemma2dlem4  25862  colinearalg  26613  upgrwlkdvdelem  27434  umgr2wlk  27645  clwwlknwwlksn  27733  clwwlknonex2lem2  27804  dmdbr5ati  30116  cvmlift3lem4  32456  dfon2lem9  32923  fscgr  33428  colinbtwnle  33466  broutsideof2  33470  a1i14  33535  a1i24  33536  ordcmp  33682  bj-peircestab  33775  wl-aleq  34646  itg2addnc  34816  filbcmb  34886  mpobi123f  35311  mptbi12f  35315  ac6s6  35321  ltrnid  37141  cdleme25dN  37362  nn0rppwr  39050  ntrneiiso  40309  ee323  40710  vd13  40803  vd23  40804  ee03  40943  ee23an  40959  ee32  40961  ee32an  40963  ee123  40965  iccpartgt  43422  stgoldbwt  43776  tgoldbach  43817  nzerooringczr  44178
  Copyright terms: Public domain W3C validator