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  1737  equvel  2460  propeqop  5455  funopsn  7093  xpexr  7860  resf1extb  7876  omordi  8493  omwordi  8498  odi  8506  omass  8507  oen0  8514  oewordi  8519  oewordri  8520  nnmwordi  8563  omabs  8579  fisupg  9188  fiinfg  9404  cantnfle  9580  cantnflem1  9598  gchina  10610  nqereu  10840  supsrlem  11022  1re  11132  lemul1a  11995  xlemul1a  13203  xrsupsslem  13222  xrinfmsslem  13223  xrub  13227  supxrunb1  13234  supxrunb2  13235  difelfzle  13557  addmodlteq  13869  seqcl2  13943  facdiv  14210  facwordi  14212  faclbnd  14213  pfxccat3  14657  dvdsabseq  16240  nn0rppwr  16488  divgcdcoprm0  16592  2mulprm  16620  exprmfct  16631  prmfac1  16647  pockthg  16834  nzerooringczr  21435  cply1mul  22240  mdetralt  22552  cmpsub  23344  fbfinnfr  23785  alexsubALTlem2  23992  alexsubALTlem3  23993  ovolicc2lem3  25476  dvfsumlem2  25989  fta1g  26131  fta1  26272  taylply2  26331  mulcxp  26650  cxpcn3lem  26713  gausslemma2dlem4  27336  colinearalg  28983  upgrwlkdvdelem  29809  umgr2wlk  30022  clwwlknwwlksn  30113  clwwlknonex2lem2  30183  dmdbr5ati  32497  cvmlift3lem4  35516  antnestlaw2  35886  dfon2lem9  35983  fscgr  36274  colinbtwnle  36312  broutsideof2  36316  a1i14  36494  a1i24  36495  ordcmp  36641  bj-peircestab  36753  wl-aleq  37740  itg2addnc  37875  filbcmb  37941  mpobi123f  38363  mptbi12f  38367  ac6s6  38373  ltrnid  40395  cdleme25dN  40616  ntrneiiso  44332  ee323  44749  vd13  44842  vd23  44843  ee03  44981  ee23an  44997  ee32  44999  ee32an  45001  ee123  45003  iccpartgt  47673  stgoldbwt  48022  tgoldbach  48063  gpgedg2iv  48313