MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  a1dd Structured version   Visualization version   GIF version

Theorem a1dd 48
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 34 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  49  ad4ant13  1284  ad4ant124  1287  ad4ant23  1289  merco2  1652  equvel  2335  propeqop  4895  funopsn  6319  xpexr  6999  omordi  7533  omwordi  7538  odi  7546  omass  7547  oen0  7553  oewordi  7558  oewordri  7559  nnmwordi  7602  omabs  7614  fisupg  8093  fiinfg  8288  cantnfle  8451  cantnflem1  8469  pr2ne  8711  gchina  9400  nqereu  9630  supsrlem  9811  1re  9918  lemul1a  10756  nnsub  10936  xlemul1a  11990  xrsupsslem  12009  xrinfmsslem  12010  xrub  12014  supxrunb1  12021  supxrunb2  12022  difelfzle  12321  addmodlteq  12607  seqcl2  12681  facdiv  12936  facwordi  12938  faclbnd  12939  swrdswrdlem  13311  swrdccat3  13343  dvdsabseq  14873  divgcdcoprm0  15217  exprmfct  15254  prmfac1  15269  pockthg  15448  cply1mul  19485  mdetralt  20233  cmpsub  21013  fbfinnfr  21455  alexsubALTlem2  21662  alexsubALTlem3  21663  ovolicc2lem3  23094  fta1g  23731  fta1  23867  mulcxp  24231  cxpcn3lem  24288  gausslemma2dlem4  24894  colinearalg  25590  vdn0frgrav2  26550  vdgn0frgrav2  26551  2spotmdisj  26595  numclwwlkovf2ex  26613  dmdbr5ati  28665  cvmlift3lem4  30558  dfon2lem9  30940  fscgr  31357  colinbtwnle  31395  broutsideof2  31399  a1i14  31464  a1i24  31465  ordcmp  31616  wl-aleq  32501  itg2addnc  32634  filbcmb  32705  mpt2bi123f  33141  mptbi12f  33145  ac6s6  33150  ltrnid  34439  cdleme25dN  34662  ntrneiiso  37409  ee323  37735  vd13  37847  vd23  37848  ee03  37989  ee23an  38005  ee32  38007  ee32an  38009  ee123  38011  iccpartgt  39965  stgoldbwt  40198  tgoldbach  40232  tgoldbachOLD  40239  pfxccat3  40289  upgrwlkdvdelem  40942  umgr2wlk  41156  av-extwwlkfablem2  41510  av-numclwwlkovf2ex  41517  nzerooringczr  41864
  Copyright terms: Public domain W3C validator