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  1771  cbv1v  1773  ralimdaa  2576  reuss2  3464  finds2  4670  ssrel  4784  ssrel2  4786  ssrelrel  4796  funfvima2  5845  tfrlem1  6424  tfrlemi1  6448  tfr1onlemaccex  6464  tfrcllemaccex  6477  tfri3  6483  nneneq  6986  ac6sfi  7028  nnnninfeq  7263  nnnninfeq2  7264  pitonn  8003  nnaddcl  9098  nnmulcl  9099  zaddcllempos  9451  zaddcllemneg  9453  peano5uzti  9523  uzind2  9527  fzind  9530  zindd  9533  uzaddcl  9749  exfzdc  10413  frec2uzltd  10592  frecuzrdgg  10605  seq3val  10649  seqvalcd  10650  seq3clss  10660  monoord  10674  seq3caopr3  10680  seqcaopr3g  10681  seq3f1olemp  10704  seqf1oglem2a  10707  seqf1og  10710  seq3id3  10713  seq3homo  10716  seq3z  10717  seqfeq4g  10720  ser3ge0  10725  exp3vallem  10729  expcllem  10739  expap0  10758  mulexp  10767  expadd  10770  expmul  10773  leexp2r  10782  leexp1a  10783  bernneq  10849  modqexp  10855  nn0ltexp2  10898  apexp1  10907  facdiv  10927  facwordi  10929  faclbnd  10930  faclbnd6  10933  omgadd  10991  seq3coll  11031  cjexp  11370  resqrexlemover  11487  resqrexlemdecn  11489  resqrexlemlo  11490  resqrexlemcalc3  11493  absexp  11556  fsum2d  11912  modfsummod  11935  fsumabs  11942  fsumiun  11954  binom  11961  bcxmas  11966  cvgratnnlemnexp  12001  cvgratnnlemmn  12002  clim2prod  12016  prodfap0  12022  prodfrecap  12023  fprodabs  12093  fprod2d  12100  demoivreALT  12251  dvdsfac  12337  bitsinv1  12439  gcdmultiple  12507  rplpwr  12514  nn0seqcvgd  12529  alginv  12535  algcvga  12539  algfx  12540  prmdvdsexp  12636  prmfac1  12640  eulerthlemrprm  12717  eulerthlema  12718  pcmpt  12832  pcfac  12839  prmpwdvds  12844  ennnfoneleminc  12948  ennnfonelemkh  12949  ennnfonelemhf1o  12950  ennnfonelemhom  12952  nninfdclemlt  12988  gsumfzz  13494  mulgnnass  13660  mhmmulg  13666  gsumfzconst  13844  srgmulgass  13918  srgpcomp  13919  lmodvsmmulgdi  14252  cnfldexp  14506  gsumfzfsumlemm  14516  tgcl  14703  dvmptfsum  15364  plycolemc  15397  rpcxpmul2  15552  lgsquad2lem2  15726  nninfsellemdc  16287  nnnninfex  16299