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

Step	Hyp	Ref	Expression
1		a1dd.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		ax-1 6	. 2 ⊢ (𝜒 → (𝜃 → 𝜒))
3	1, 2	syl6 35	1 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

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  1740  equvel  2456  propeqop  5415  funopsn  7002  xpexr  7739  omordi  8359  omwordi  8364  odi  8372  omass  8373  oen0  8379  oewordi  8384  oewordri  8385  nnmwordi  8428  omabs  8441  fisupg  8992  fiinfg  9188  cantnfle  9359  cantnflem1  9377  pr2ne  9692  gchina  10386  nqereu  10616  supsrlem  10798  1re  10906  lemul1a  11759  xlemul1a  12951  xrsupsslem  12970  xrinfmsslem  12971  xrub  12975  supxrunb1  12982  supxrunb2  12983  difelfzle  13298  addmodlteq  13594  seqcl2  13669  facdiv  13929  facwordi  13931  faclbnd  13932  pfxccat3  14375  dvdsabseq  15950  divgcdcoprm0  16298  2mulprm  16326  exprmfct  16337  prmfac1  16354  pockthg  16535  cply1mul  21375  mdetralt  21665  cmpsub  22459  fbfinnfr  22900  alexsubALTlem2  23107  alexsubALTlem3  23108  ovolicc2lem3  24588  fta1g  25237  fta1  25373  mulcxp  25745  cxpcn3lem  25805  gausslemma2dlem4  26422  colinearalg  27181  upgrwlkdvdelem  28005  umgr2wlk  28215  clwwlknwwlksn  28303  clwwlknonex2lem2  28373  dmdbr5ati  30685  cvmlift3lem4  33184  dfon2lem9  33673  fscgr  34309  colinbtwnle  34347  broutsideof2  34351  a1i14  34416  a1i24  34417  ordcmp  34563  bj-peircestab  34660  wl-aleq  35621  itg2addnc  35758  filbcmb  35825  mpobi123f  36247  mptbi12f  36251  ac6s6  36257  ltrnid  38076  cdleme25dN  38297  nn0rppwr  40254  ntrneiiso  41590  ee323  42017  vd13  42110  vd23  42111  ee03  42250  ee23an  42266  ee32  42268  ee32an  42270  ee123  42272  iccpartgt  44767  stgoldbwt  45116  tgoldbach  45157  nzerooringczr  45518