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 ⊢ (𝜑 → (𝜓 → (𝜃 → 𝜒)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  2a1dd  52  merco2  1769  equvel  2490  propeqop  5492  funopsnOLD  7151  xpexr  7921  resf1extb  7937  omordi  8557  omwordi  8562  odi  8570  omass  8571  oen0  8578  oewordi  8583  oewordri  8584  nnmwordi  8627  omabs  8643  fisupg  9255  fiinfg  9468  cantnfle  9647  cantnflem1  9665  gchina  10701  nqereu  10931  supsrlem  11113  1re  11225  lemul1a  12086  xlemul1a  13332  xrsupsslem  13351  xrinfmsslem  13352  xrub  13356  supxrunb1  13363  supxrunb2  13364  difelfzle  13688  addmodlteq  14002  seqcl2  14076  facdiv  14343  facwordi  14345  faclbnd  14346  pfxccat3  14795  dvdsabseq  16395  nn0rppwr  16643  divgcdcoprm0  16747  2mulprm  16775  exprmfct  16787  prmfac1  16803  pockthg  16990  nzerooringczr  21682  cply1mul  22508  mdetralt  22817  cmpsub  23609  fbfinnfr  24051  alexsubALTlem2  24258  alexsubALTlem3  24259  ovolicc2lem3  25731  dvfsumlem2  26239  fta1g  26380  fta1  26522  taylply2  26584  mulcxp  26903  cxpcn3lem  26965  gausslemma2dlem4  27586  colinearalg  29317  upgrwlkdvdelem  30151  umgr2wlk  30367  clwwlknwwlksn  30458  clwwlknonex2lem2  30528  dmdbr5ati  32847  cvmlift3lem4  35853  antnestlaw2  36223  dfon2lem9  36320  fscgr  36611  colinbtwnle  36649  broutsideof2  36653  a1i14  36871  a1i24  36872  ordcmp  37017  bj-peircestab  37202  wl-aleq  38249  itg2addnc  38384  filbcmb  38451  mpobi123f  38871  mptbi12f  38875  ac6s6  38881  ltrnid  40969  cdleme25dN  41190  ntrneiiso  44877  ee323  45277  vd13  45370  vd23  45371  ee03  45509  ee23an  45525  ee32  45527  ee32an  45529  ee123  45531  iccpartgt  48236  stgoldbwt  48601  tgoldbach  48642  gpgedg2iv  48892