Theorem a2d 26

Description: Deduction distributing an embedded antecedent. (Contributed by NM, 23-Jun-1994.)

Hypothesis

Ref	Expression
a2d.1	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Assertion

Ref	Expression
a2d	⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

Proof of Theorem a2d

Step	Hyp	Ref	Expression
1		a2d.1	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
2		ax-2 6	. 2 ⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
3	1, 2	syl 14	1 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  mpdd  41  imim2d  54  imim3i  61  loowoz  102  animpimp2impd  527  cbv1  1686  ralimdaa  2452  reuss2  3295  finds2  4444  ssrel  4555  ssrel2  4557  ssrelrel  4567  funfvima2  5566  tfrlem1  6111  tfrlemi1  6135  tfr1onlemaccex  6151  tfrcllemaccex  6164  tfri3  6170  nneneq  6653  ac6sfi  6694  pitonn  7482  nnaddcl  8540  nnmulcl  8541  zaddcllempos  8885  zaddcllemneg  8887  peano5uzti  8953  uzind2  8957  fzind  8960  zindd  8963  uzaddcl  9173  exfzdc  9800  frec2uzltd  9959  frecuzrdgg  9972  seq3val  10013  seq3clss  10017  monoord  10026  seq3caopr3  10031  seq3f1olemp  10052  seq3id3  10057  seq3homo  10060  seq3z  10061  ser3ge0  10067  exp3vallem  10071  expcllem  10081  expap0  10100  mulexp  10109  expadd  10112  expmul  10115  leexp2r  10124  leexp1a  10125  bernneq  10189  facdiv  10261  facwordi  10263  faclbnd  10264  faclbnd6  10267  omgadd  10325  seq3coll  10362  cjexp  10442  resqrexlemover  10558  resqrexlemdecn  10560  resqrexlemlo  10561  resqrexlemcalc3  10564  absexp  10627  fsum2d  10978  modfsummod  11001  fsumabs  11008  fsumiun  11020  binom  11027  bcxmas  11032  cvgratnnlemnexp  11067  cvgratnnlemmn  11068  demoivreALT  11212  dvdsfac  11288  gcdmultiple  11436  rplpwr  11443  nn0seqcvgd  11450  alginv  11456  algcvga  11460  algfx  11461  prmdvdsexp  11554  prmfac1  11558  tgcl  11916  nninfalllemn  12603  nninfsellemdc  12607