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

Theorem a1dd 47
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  48  ad4ant13  1283  ad4ant124  1286  ad4ant23  1288  merco2  1651  equvel  2334  xpexr  6976  omordi  7510  omwordi  7515  odi  7523  omass  7524  oen0  7530  oewordi  7535  oewordri  7536  nnmwordi  7579  omabs  7591  fisupg  8070  fiinfg  8265  cantnfle  8428  cantnflem1  8446  pr2ne  8688  gchina  9377  nqereu  9607  supsrlem  9788  1re  9895  lemul1a  10728  nnsub  10908  xlemul1a  11949  xrsupsslem  11967  xrinfmsslem  11968  xrub  11972  supxrunb1  11979  supxrunb2  11980  difelfzle  12278  addmodlteq  12564  seqcl2  12638  facdiv  12893  facwordi  12895  faclbnd  12896  swrdswrdlem  13259  swrdccat3  13291  dvdsabseq  14821  divgcdcoprm0  15165  exprmfct  15202  prmfac1  15217  pockthg  15396  cply1mul  19433  mdetralt  20180  cmpsub  20960  fbfinnfr  21402  alexsubALTlem2  21609  alexsubALTlem3  21610  ovolicc2lem3  23038  fta1g  23675  fta1  23811  mulcxp  24175  cxpcn3lem  24232  gausslemma2dlem4  24838  colinearalg  25535  vdn0frgrav2  26343  vdgn0frgrav2  26344  2spotmdisj  26388  numclwwlkovf2ex  26406  dmdbr5ati  28458  cvmlift3lem4  30351  dfon2lem9  30733  fscgr  31150  colinbtwnle  31188  broutsideof2  31192  a1i14  31257  a1i24  31258  ordcmp  31409  wl-aleq  32284  itg2addnc  32417  filbcmb  32488  mpt2bi123f  32924  mptbi12f  32928  ac6s6  32933  ltrnid  34222  cdleme25dN  34445  ntrneiiso  37192  ee323  37518  vd13  37630  vd23  37631  ee03  37772  ee23an  37788  ee32  37790  ee32an  37792  ee123  37794  iccpartgt  39749  stgoldbwt  39982  tgoldbach  40016  tgoldbachOLD  40023  pfxccat3  40073  propeqop  40105  funopsn  40123  upgrwlkdvdelem  40923  umgr2wlk  41137  av-extwwlkfablem2  41491  av-numclwwlkovf2ex  41498  nzerooringczr  41845
  Copyright terms: Public domain W3C validator