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  1739  equvel  2455  propeqop  5469  funopsn  7099  xpexr  7860  omordi  8518  omwordi  8523  odi  8531  omass  8532  oen0  8538  oewordi  8543  oewordri  8544  nnmwordi  8587  omabs  8602  fisupg  9242  fiinfg  9442  cantnfle  9614  cantnflem1  9632  pr2neOLD  9948  gchina  10642  nqereu  10872  supsrlem  11054  1re  11162  lemul1a  12016  xlemul1a  13214  xrsupsslem  13233  xrinfmsslem  13234  xrub  13238  supxrunb1  13245  supxrunb2  13246  difelfzle  13561  addmodlteq  13858  seqcl2  13933  facdiv  14194  facwordi  14196  faclbnd  14197  pfxccat3  14629  dvdsabseq  16202  divgcdcoprm0  16548  2mulprm  16576  exprmfct  16587  prmfac1  16604  pockthg  16785  cply1mul  21681  mdetralt  21973  cmpsub  22767  fbfinnfr  23208  alexsubALTlem2  23415  alexsubALTlem3  23416  ovolicc2lem3  24899  fta1g  25548  fta1  25684  mulcxp  26056  cxpcn3lem  26116  gausslemma2dlem4  26733  colinearalg  27901  upgrwlkdvdelem  28726  umgr2wlk  28936  clwwlknwwlksn  29024  clwwlknonex2lem2  29094  dmdbr5ati  31406  cvmlift3lem4  33956  dfon2lem9  34405  fscgr  34694  colinbtwnle  34732  broutsideof2  34736  a1i14  34801  a1i24  34802  ordcmp  34948  bj-peircestab  35045  wl-aleq  36023  itg2addnc  36161  filbcmb  36228  mpobi123f  36650  mptbi12f  36654  ac6s6  36660  ltrnid  38627  cdleme25dN  38848  nn0rppwr  40848  ntrneiiso  42437  ee323  42864  vd13  42957  vd23  42958  ee03  43097  ee23an  43113  ee32  43115  ee32an  43117  ee123  43119  iccpartgt  45693  stgoldbwt  46042  tgoldbach  46083  nzerooringczr  46444
  Copyright terms: Public domain W3C validator