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  4694  ssrel  4809  ssrel2  4811  ssrelrel  4821  funfvima2  5879  tfrlem1  6465  tfrlemi1  6489  tfr1onlemaccex  6505  tfrcllemaccex  6518  tfri3  6524  nneneq  7031  ac6sfi  7073  nnnninfeq  7311  nnnninfeq2  7312  pitonn  8051  nnaddcl  9146  nnmulcl  9147  zaddcllempos  9499  zaddcllemneg  9501  peano5uzti  9571  uzind2  9575  fzind  9578  zindd  9581  uzaddcl  9798  exfzdc  10463  frec2uzltd  10642  frecuzrdgg  10655  seq3val  10699  seqvalcd  10700  seq3clss  10710  monoord  10724  seq3caopr3  10730  seqcaopr3g  10731  seq3f1olemp  10754  seqf1oglem2a  10757  seqf1og  10760  seq3id3  10763  seq3homo  10766  seq3z  10767  seqfeq4g  10770  ser3ge0  10775  exp3vallem  10779  expcllem  10789  expap0  10808  mulexp  10817  expadd  10820  expmul  10823  leexp2r  10832  leexp1a  10833  bernneq  10899  modqexp  10905  nn0ltexp2  10948  apexp1  10957  facdiv  10977  facwordi  10979  faclbnd  10980  faclbnd6  10983  omgadd  11041  seq3coll  11082  cjexp  11425  resqrexlemover  11542  resqrexlemdecn  11544  resqrexlemlo  11545  resqrexlemcalc3  11548  absexp  11611  fsum2d  11967  modfsummod  11990  fsumabs  11997  fsumiun  12009  binom  12016  bcxmas  12021  cvgratnnlemnexp  12056  cvgratnnlemmn  12057  clim2prod  12071  prodfap0  12077  prodfrecap  12078  fprodabs  12148  fprod2d  12155  demoivreALT  12306  dvdsfac  12392  bitsinv1  12494  gcdmultiple  12562  rplpwr  12569  nn0seqcvgd  12584  alginv  12590  algcvga  12594  algfx  12595  prmdvdsexp  12691  prmfac1  12695  eulerthlemrprm  12772  eulerthlema  12773  pcmpt  12887  pcfac  12894  prmpwdvds  12899  ennnfoneleminc  13003  ennnfonelemkh  13004  ennnfonelemhf1o  13005  ennnfonelemhom  13007  nninfdclemlt  13043  gsumfzz  13549  mulgnnass  13715  mhmmulg  13721  gsumfzconst  13899  srgmulgass  13973  srgpcomp  13974  lmodvsmmulgdi  14308  cnfldexp  14562  gsumfzfsumlemm  14572  tgcl  14759  dvmptfsum  15420  plycolemc  15453  rpcxpmul2  15608  lgsquad2lem2  15782  nninfsellemdc  16490  nnnninfex  16502