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  1791  cbv1v  1793  ralimdaa  2596  reuss2  3484  finds2  4693  ssrel  4807  ssrel2  4809  ssrelrel  4819  funfvima2  5876  tfrlem1  6460  tfrlemi1  6484  tfr1onlemaccex  6500  tfrcllemaccex  6513  tfri3  6519  nneneq  7026  ac6sfi  7068  nnnninfeq  7303  nnnninfeq2  7304  pitonn  8043  nnaddcl  9138  nnmulcl  9139  zaddcllempos  9491  zaddcllemneg  9493  peano5uzti  9563  uzind2  9567  fzind  9570  zindd  9573  uzaddcl  9789  exfzdc  10454  frec2uzltd  10633  frecuzrdgg  10646  seq3val  10690  seqvalcd  10691  seq3clss  10701  monoord  10715  seq3caopr3  10721  seqcaopr3g  10722  seq3f1olemp  10745  seqf1oglem2a  10748  seqf1og  10751  seq3id3  10754  seq3homo  10757  seq3z  10758  seqfeq4g  10761  ser3ge0  10766  exp3vallem  10770  expcllem  10780  expap0  10799  mulexp  10808  expadd  10811  expmul  10814  leexp2r  10823  leexp1a  10824  bernneq  10890  modqexp  10896  nn0ltexp2  10939  apexp1  10948  facdiv  10968  facwordi  10970  faclbnd  10971  faclbnd6  10974  omgadd  11032  seq3coll  11072  cjexp  11412  resqrexlemover  11529  resqrexlemdecn  11531  resqrexlemlo  11532  resqrexlemcalc3  11535  absexp  11598  fsum2d  11954  modfsummod  11977  fsumabs  11984  fsumiun  11996  binom  12003  bcxmas  12008  cvgratnnlemnexp  12043  cvgratnnlemmn  12044  clim2prod  12058  prodfap0  12064  prodfrecap  12065  fprodabs  12135  fprod2d  12142  demoivreALT  12293  dvdsfac  12379  bitsinv1  12481  gcdmultiple  12549  rplpwr  12556  nn0seqcvgd  12571  alginv  12577  algcvga  12581  algfx  12582  prmdvdsexp  12678  prmfac1  12682  eulerthlemrprm  12759  eulerthlema  12760  pcmpt  12874  pcfac  12881  prmpwdvds  12886  ennnfoneleminc  12990  ennnfonelemkh  12991  ennnfonelemhf1o  12992  ennnfonelemhom  12994  nninfdclemlt  13030  gsumfzz  13536  mulgnnass  13702  mhmmulg  13708  gsumfzconst  13886  srgmulgass  13960  srgpcomp  13961  lmodvsmmulgdi  14295  cnfldexp  14549  gsumfzfsumlemm  14559  tgcl  14746  dvmptfsum  15407  plycolemc  15440  rpcxpmul2  15595  lgsquad2lem2  15769  nninfsellemdc  16406  nnnninfex  16418