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  ad4ant13  1289  ad4ant124  1292  ad4ant23  1294  merco2  1658  equvel  2346  propeqop  4940  funopsn  6378  xpexr  7068  omordi  7606  omwordi  7611  odi  7619  omass  7620  oen0  7626  oewordi  7631  oewordri  7632  nnmwordi  7675  omabs  7687  fisupg  8168  fiinfg  8365  cantnfle  8528  cantnflem1  8546  pr2ne  8788  gchina  9481  nqereu  9711  supsrlem  9892  1re  9999  lemul1a  10837  nnsub  11019  xlemul1a  12077  xrsupsslem  12096  xrinfmsslem  12097  xrub  12101  supxrunb1  12108  supxrunb2  12109  difelfzle  12409  addmodlteq  12701  seqcl2  12775  facdiv  13030  facwordi  13032  faclbnd  13033  swrdswrdlem  13413  swrdccat3  13445  dvdsabseq  14978  divgcdcoprm0  15322  exprmfct  15359  prmfac1  15374  pockthg  15553  cply1mul  19604  mdetralt  20354  cmpsub  21143  fbfinnfr  21585  alexsubALTlem2  21792  alexsubALTlem3  21793  ovolicc2lem3  23227  fta1g  23865  fta1  24001  mulcxp  24365  cxpcn3lem  24422  gausslemma2dlem4  25028  colinearalg  25724  upgrwlkdvdelem  26535  umgr2wlk  26748  extwwlkfablem2  27102  numclwwlkovf2ex  27109  dmdbr5ati  29169  cvmlift3lem4  31065  dfon2lem9  31450  fscgr  31882  colinbtwnle  31920  broutsideof2  31924  a1i14  31989  a1i24  31990  ordcmp  32141  wl-aleq  32993  itg2addnc  33135  filbcmb  33206  mpt2bi123f  33642  mptbi12f  33646  ac6s6  33651  ltrnid  34940  cdleme25dN  35163  ntrneiiso  37910  ee323  38235  vd13  38347  vd23  38348  ee03  38489  ee23an  38505  ee32  38507  ee32an  38509  ee123  38511  iccpartgt  40691  pfxccat3  40755  stgoldbwt  40989  tgoldbach  41023  tgoldbachOLD  41030  nzerooringczr  41390
 Copyright terms: Public domain W3C validator