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 7	. 2 ⊢ ((𝜓 → (𝜒 → 𝜃)) → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))
3	1, 2	syl 14	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:  mpdd  41  imim2d  54  imim3i  61  loowoz  103  animpimp2impd  559  cbv1  1745  cbv1v  1747  ralimdaa  2543  reuss2  3416  finds2  4601  ssrel  4715  ssrel2  4717  ssrelrel  4727  funfvima2  5750  tfrlem1  6309  tfrlemi1  6333  tfr1onlemaccex  6349  tfrcllemaccex  6362  tfri3  6368  nneneq  6857  ac6sfi  6898  nnnninfeq  7126  nnnninfeq2  7127  pitonn  7847  nnaddcl  8939  nnmulcl  8940  zaddcllempos  9290  zaddcllemneg  9292  peano5uzti  9361  uzind2  9365  fzind  9368  zindd  9371  uzaddcl  9586  exfzdc  10240  frec2uzltd  10403  frecuzrdgg  10416  seq3val  10458  seqvalcd  10459  seq3clss  10467  monoord  10476  seq3caopr3  10481  seq3f1olemp  10502  seq3id3  10507  seq3homo  10510  seq3z  10511  ser3ge0  10517  exp3vallem  10521  expcllem  10531  expap0  10550  mulexp  10559  expadd  10562  expmul  10565  leexp2r  10574  leexp1a  10575  bernneq  10641  modqexp  10647  nn0ltexp2  10689  apexp1  10698  facdiv  10718  facwordi  10720  faclbnd  10721  faclbnd6  10724  omgadd  10782  seq3coll  10822  cjexp  10902  resqrexlemover  11019  resqrexlemdecn  11021  resqrexlemlo  11022  resqrexlemcalc3  11025  absexp  11088  fsum2d  11443  modfsummod  11466  fsumabs  11473  fsumiun  11485  binom  11492  bcxmas  11497  cvgratnnlemnexp  11532  cvgratnnlemmn  11533  clim2prod  11547  prodfap0  11553  prodfrecap  11554  fprodabs  11624  fprod2d  11631  demoivreALT  11781  dvdsfac  11866  gcdmultiple  12021  rplpwr  12028  nn0seqcvgd  12041  alginv  12047  algcvga  12051  algfx  12052  prmdvdsexp  12148  prmfac1  12152  eulerthlemrprm  12229  eulerthlema  12230  pcmpt  12341  pcfac  12348  prmpwdvds  12353  ennnfoneleminc  12412  ennnfonelemkh  12413  ennnfonelemhf1o  12414  ennnfonelemhom  12416  nninfdclemlt  12452  mulgnnass  13018  mhmmulg  13024  srgmulgass  13172  srgpcomp  13173  lmodvsmmulgdi  13413  cnfldexp  13474  tgcl  13567  nninfsellemdc  14762