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  561  cbv1  1792  cbv1v  1794  ralimdaa  2597  reuss2  3486  finds2  4701  ssrel  4816  ssrel2  4818  ssrelrel  4828  funfvima2  5892  tfrlem1  6479  tfrlemi1  6503  tfr1onlemaccex  6519  tfrcllemaccex  6532  tfri3  6538  nneneq  7048  ac6sfi  7092  nnnninfeq  7332  nnnninfeq2  7333  pitonn  8073  nnaddcl  9168  nnmulcl  9169  zaddcllempos  9521  zaddcllemneg  9523  peano5uzti  9593  uzind2  9597  fzind  9600  zindd  9603  uzaddcl  9825  exfzdc  10492  frec2uzltd  10671  frecuzrdgg  10684  seq3val  10728  seqvalcd  10729  seq3clss  10739  monoord  10753  seq3caopr3  10759  seqcaopr3g  10760  seq3f1olemp  10783  seqf1oglem2a  10786  seqf1og  10789  seq3id3  10792  seq3homo  10795  seq3z  10796  seqfeq4g  10799  ser3ge0  10804  exp3vallem  10808  expcllem  10818  expap0  10837  mulexp  10846  expadd  10849  expmul  10852  leexp2r  10861  leexp1a  10862  bernneq  10928  modqexp  10934  nn0ltexp2  10977  apexp1  10986  facdiv  11006  facwordi  11008  faclbnd  11009  faclbnd6  11012  omgadd  11071  seq3coll  11112  cjexp  11476  resqrexlemover  11593  resqrexlemdecn  11595  resqrexlemlo  11596  resqrexlemcalc3  11599  absexp  11662  fsum2d  12019  modfsummod  12042  fsumabs  12049  fsumiun  12061  binom  12068  bcxmas  12073  cvgratnnlemnexp  12108  cvgratnnlemmn  12109  clim2prod  12123  prodfap0  12129  prodfrecap  12130  fprodabs  12200  fprod2d  12207  demoivreALT  12358  dvdsfac  12444  bitsinv1  12546  gcdmultiple  12614  rplpwr  12621  nn0seqcvgd  12636  alginv  12642  algcvga  12646  algfx  12647  prmdvdsexp  12743  prmfac1  12747  eulerthlemrprm  12824  eulerthlema  12825  pcmpt  12939  pcfac  12946  prmpwdvds  12951  ennnfoneleminc  13055  ennnfonelemkh  13056  ennnfonelemhf1o  13057  ennnfonelemhom  13059  nninfdclemlt  13095  gsumfzz  13601  mulgnnass  13767  mhmmulg  13773  gsumfzconst  13951  srgmulgass  14026  srgpcomp  14027  lmodvsmmulgdi  14361  cnfldexp  14615  gsumfzfsumlemm  14625  tgcl  14817  dvmptfsum  15478  plycolemc  15511  rpcxpmul2  15666  lgsquad2lem2  15840  eupth2lemsfi  16358  eupth2fi  16359  depindlem2  16387  depindlem3  16388  nninfsellemdc  16675  nnnninfex  16687