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  1743  equvel  2455  propeqop  5361  funopsn  6914  xpexr  7642  omordi  8216  omwordi  8221  odi  8229  omass  8230  oen0  8236  oewordi  8241  oewordri  8242  nnmwordi  8285  omabs  8298  fisupg  8833  fiinfg  9029  cantnfle  9200  cantnflem1  9218  pr2ne  9498  gchina  10192  nqereu  10422  supsrlem  10604  1re  10712  lemul1a  11565  xlemul1a  12757  xrsupsslem  12776  xrinfmsslem  12777  xrub  12781  supxrunb1  12788  supxrunb2  12789  difelfzle  13104  addmodlteq  13398  seqcl2  13473  facdiv  13732  facwordi  13734  faclbnd  13735  pfxccat3  14178  dvdsabseq  15751  divgcdcoprm0  16099  2mulprm  16127  exprmfct  16138  prmfac1  16155  pockthg  16335  cply1mul  21062  mdetralt  21352  cmpsub  22144  fbfinnfr  22585  alexsubALTlem2  22792  alexsubALTlem3  22793  ovolicc2lem3  24264  fta1g  24912  fta1  25048  mulcxp  25420  cxpcn3lem  25480  gausslemma2dlem4  26097  colinearalg  26848  upgrwlkdvdelem  27669  umgr2wlk  27879  clwwlknwwlksn  27967  clwwlknonex2lem2  28037  dmdbr5ati  30349  cvmlift3lem4  32847  dfon2lem9  33331  fscgr  34012  colinbtwnle  34050  broutsideof2  34054  a1i14  34119  a1i24  34120  ordcmp  34266  bj-peircestab  34363  wl-aleq  35306  itg2addnc  35443  filbcmb  35510  mpobi123f  35932  mptbi12f  35936  ac6s6  35942  ltrnid  37761  cdleme25dN  37982  nn0rppwr  39894  ntrneiiso  41231  ee323  41650  vd13  41743  vd23  41744  ee03  41883  ee23an  41899  ee32  41901  ee32an  41903  ee123  41905  iccpartgt  44397  stgoldbwt  44746  tgoldbach  44787  nzerooringczr  45148