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  2488  propeqop  5486  funopsnOLD  7184  xpexr  7964  resf1extb  7980  omordi  8612  omwordi  8617  odi  8625  omass  8626  oen0  8633  oewordi  8638  oewordri  8639  nnmwordi  8682  omabs  8698  fisupg  9317  fiinfg  9530  cantnfle  9709  cantnflem1  9727  gchina  10823  nqereu  11053  supsrlem  11235  1re  11347  lemul1a  12211  xlemul1a  13458  xrsupsslem  13477  xrinfmsslem  13478  xrub  13482  supxrunb1  13489  supxrunb2  13490  difelfzle  13815  addmodlteq  14129  seqcl2  14203  facdiv  14472  facwordi  14474  faclbnd  14475  pfxccat3  14925  dvdsabseq  16527  nn0rppwr  16779  divgcdcoprm0  16884  2mulprm  16912  exprmfct  16924  prmfac1  16940  pockthg  17128  nzerooringczr  21841  cply1mul  22669  mdetralt  22978  cmpsub  23773  fbfinnfr  24215  alexsubALTlem2  24422  alexsubALTlem3  24423  ovolicc2lem3  25895  dvfsumlem2  26402  fta1g  26543  fta1  26684  taylply2  26752  mulcxp  27070  cxpcn3lem  27132  gausslemma2dlem4  27753  colinearalg  29545  upgrwlkdvdelem  30379  umgr2wlk  30595  clwwlknwwlksn  30686  clwwlknonex2lem2  30756  dmdbr5ati  33081  cvmlift3lem4  36295  antnestlaw2  36665  dfon2lem9  36768  fscgr  37060  colinbtwnle  37098  broutsideof2  37102  a1i14  37304  a1i24  37305  ordcmp  37450  bj-peircestab  37635  wl-aleq  38735  itg2addnc  38860  filbcmb  38940  mpobi123f  39360  mptbi12f  39364  ac6s6  39370  ltrnid  41458  cdleme25dN  41679  ntrneiiso  45352  ee323  45751  vd13  45844  vd23  45845  ee03  45983  ee23an  45999  ee32  46001  ee32an  46003  ee123  46005  tmachlem-agreeprod  48220  iccpartgt  48782  stgoldbwt  49147  tgoldbach  49188  gpgedg2iv  49438  lazsubcl  49739