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  1739  equvel  2456  propeqop  5421  funopsn  7020  xpexr  7765  omordi  8397  omwordi  8402  odi  8410  omass  8411  oen0  8417  oewordi  8422  oewordri  8423  nnmwordi  8466  omabs  8481  fisupg  9062  fiinfg  9258  cantnfle  9429  cantnflem1  9447  pr2ne  9761  gchina  10455  nqereu  10685  supsrlem  10867  1re  10975  lemul1a  11829  xlemul1a  13022  xrsupsslem  13041  xrinfmsslem  13042  xrub  13046  supxrunb1  13053  supxrunb2  13054  difelfzle  13369  addmodlteq  13666  seqcl2  13741  facdiv  14001  facwordi  14003  faclbnd  14004  pfxccat3  14447  dvdsabseq  16022  divgcdcoprm0  16370  2mulprm  16398  exprmfct  16409  prmfac1  16426  pockthg  16607  cply1mul  21465  mdetralt  21757  cmpsub  22551  fbfinnfr  22992  alexsubALTlem2  23199  alexsubALTlem3  23200  ovolicc2lem3  24683  fta1g  25332  fta1  25468  mulcxp  25840  cxpcn3lem  25900  gausslemma2dlem4  26517  colinearalg  27278  upgrwlkdvdelem  28104  umgr2wlk  28314  clwwlknwwlksn  28402  clwwlknonex2lem2  28472  dmdbr5ati  30784  cvmlift3lem4  33284  dfon2lem9  33767  fscgr  34382  colinbtwnle  34420  broutsideof2  34424  a1i14  34489  a1i24  34490  ordcmp  34636  bj-peircestab  34733  wl-aleq  35694  itg2addnc  35831  filbcmb  35898  mpobi123f  36320  mptbi12f  36324  ac6s6  36330  ltrnid  38149  cdleme25dN  38370  nn0rppwr  40333  ntrneiiso  41701  ee323  42128  vd13  42221  vd23  42222  ee03  42361  ee23an  42377  ee32  42379  ee32an  42381  ee123  42383  iccpartgt  44879  stgoldbwt  45228  tgoldbach  45269  nzerooringczr  45630