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  1736  equvel  2454  propeqop  5467  funopsn  7120  xpexr  7894  resf1extb  7910  omordi  8530  omwordi  8535  odi  8543  omass  8544  oen0  8550  oewordi  8555  oewordri  8556  nnmwordi  8599  omabs  8615  fisupg  9235  fiinfg  9452  cantnfle  9624  cantnflem1  9642  pr2neOLD  9958  gchina  10652  nqereu  10882  supsrlem  11064  1re  11174  lemul1a  12036  xlemul1a  13248  xrsupsslem  13267  xrinfmsslem  13268  xrub  13272  supxrunb1  13279  supxrunb2  13280  difelfzle  13602  addmodlteq  13911  seqcl2  13985  facdiv  14252  facwordi  14254  faclbnd  14255  pfxccat3  14699  dvdsabseq  16283  nn0rppwr  16531  divgcdcoprm0  16635  2mulprm  16663  exprmfct  16674  prmfac1  16690  pockthg  16877  nzerooringczr  21390  cply1mul  22183  mdetralt  22495  cmpsub  23287  fbfinnfr  23728  alexsubALTlem2  23935  alexsubALTlem3  23936  ovolicc2lem3  25420  dvfsumlem2  25933  fta1g  26075  fta1  26216  taylply2  26275  mulcxp  26594  cxpcn3lem  26657  gausslemma2dlem4  27280  colinearalg  28837  upgrwlkdvdelem  29666  umgr2wlk  29879  clwwlknwwlksn  29967  clwwlknonex2lem2  30037  dmdbr5ati  32351  cvmlift3lem4  35309  antnestlaw2  35679  dfon2lem9  35779  fscgr  36068  colinbtwnle  36106  broutsideof2  36110  a1i14  36288  a1i24  36289  ordcmp  36435  bj-peircestab  36541  wl-aleq  37523  itg2addnc  37668  filbcmb  37734  mpobi123f  38156  mptbi12f  38160  ac6s6  38166  ltrnid  40129  cdleme25dN  40350  ntrneiiso  44080  ee323  44498  vd13  44591  vd23  44592  ee03  44730  ee23an  44746  ee32  44748  ee32an  44750  ee123  44752  iccpartgt  47425  stgoldbwt  47774  tgoldbach  47815  gpgedg2iv  48055