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  3485  finds2  4697  ssrel  4812  ssrel2  4814  ssrelrel  4824  funfvima2  5882  tfrlem1  6469  tfrlemi1  6493  tfr1onlemaccex  6509  tfrcllemaccex  6522  tfri3  6528  nneneq  7038  ac6sfi  7082  nnnninfeq  7321  nnnninfeq2  7322  pitonn  8061  nnaddcl  9156  nnmulcl  9157  zaddcllempos  9509  zaddcllemneg  9511  peano5uzti  9581  uzind2  9585  fzind  9588  zindd  9591  uzaddcl  9813  exfzdc  10479  frec2uzltd  10658  frecuzrdgg  10671  seq3val  10715  seqvalcd  10716  seq3clss  10726  monoord  10740  seq3caopr3  10746  seqcaopr3g  10747  seq3f1olemp  10770  seqf1oglem2a  10773  seqf1og  10776  seq3id3  10779  seq3homo  10782  seq3z  10783  seqfeq4g  10786  ser3ge0  10791  exp3vallem  10795  expcllem  10805  expap0  10824  mulexp  10833  expadd  10836  expmul  10839  leexp2r  10848  leexp1a  10849  bernneq  10915  modqexp  10921  nn0ltexp2  10964  apexp1  10973  facdiv  10993  facwordi  10995  faclbnd  10996  faclbnd6  10999  omgadd  11058  seq3coll  11099  cjexp  11447  resqrexlemover  11564  resqrexlemdecn  11566  resqrexlemlo  11567  resqrexlemcalc3  11570  absexp  11633  fsum2d  11989  modfsummod  12012  fsumabs  12019  fsumiun  12031  binom  12038  bcxmas  12043  cvgratnnlemnexp  12078  cvgratnnlemmn  12079  clim2prod  12093  prodfap0  12099  prodfrecap  12100  fprodabs  12170  fprod2d  12177  demoivreALT  12328  dvdsfac  12414  bitsinv1  12516  gcdmultiple  12584  rplpwr  12591  nn0seqcvgd  12606  alginv  12612  algcvga  12616  algfx  12617  prmdvdsexp  12713  prmfac1  12717  eulerthlemrprm  12794  eulerthlema  12795  pcmpt  12909  pcfac  12916  prmpwdvds  12921  ennnfoneleminc  13025  ennnfonelemkh  13026  ennnfonelemhf1o  13027  ennnfonelemhom  13029  nninfdclemlt  13065  gsumfzz  13571  mulgnnass  13737  mhmmulg  13743  gsumfzconst  13921  srgmulgass  13995  srgpcomp  13996  lmodvsmmulgdi  14330  cnfldexp  14584  gsumfzfsumlemm  14594  tgcl  14781  dvmptfsum  15442  plycolemc  15475  rpcxpmul2  15630  lgsquad2lem2  15804  nninfsellemdc  16562  nnnninfex  16574