Theorem a1dd 51

Description: Double deduction introducing an antecedent. Deduction associated with a1d 26. 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 36	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  52  merco2  1766  equvel  2488  propeqop  5490  funopsnOLD  7145  xpexr  7911  resf1extb  7927  omordi  8547  omwordi  8552  odi  8560  omass  8561  oen0  8568  oewordi  8573  oewordri  8574  nnmwordi  8617  omabs  8633  fisupg  9244  fiinfg  9457  cantnfle  9636  cantnflem1  9654  gchina  10679  nqereu  10909  supsrlem  11091  1re  11203  lemul1a  12064  xlemul1a  13309  xrsupsslem  13328  xrinfmsslem  13329  xrub  13333  supxrunb1  13340  supxrunb2  13341  difelfzle  13665  addmodlteq  13978  seqcl2  14052  facdiv  14319  facwordi  14321  faclbnd  14322  pfxccat3  14767  dvdsabseq  16366  nn0rppwr  16614  divgcdcoprm0  16718  2mulprm  16746  exprmfct  16758  prmfac1  16774  pockthg  16961  nzerooringczr  21630  cply1mul  22456  mdetralt  22765  cmpsub  23557  fbfinnfr  23998  alexsubALTlem2  24205  alexsubALTlem3  24206  ovolicc2lem3  25678  dvfsumlem2  26186  fta1g  26327  fta1  26469  taylply2  26531  mulcxp  26850  cxpcn3lem  26912  gausslemma2dlem4  27533  colinearalg  29260  upgrwlkdvdelem  30085  umgr2wlk  30298  clwwlknwwlksn  30389  clwwlknonex2lem2  30459  dmdbr5ati  32774  cvmlift3lem4  35814  antnestlaw2  36184  dfon2lem9  36281  fscgr  36572  colinbtwnle  36610  broutsideof2  36614  a1i14  36812  a1i24  36813  ordcmp  36958  bj-peircestab  37143  wl-aleq  38190  itg2addnc  38325  filbcmb  38391  mpobi123f  38811  mptbi12f  38815  ac6s6  38821  ltrnid  40909  cdleme25dN  41130  ntrneiiso  44817  ee323  45217  vd13  45310  vd23  45311  ee03  45449  ee23an  45465  ee32  45467  ee32an  45469  ee123  45471  iccpartgt  48176  stgoldbwt  48541  tgoldbach  48582  gpgedg2iv  48832