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  1756  cbv1v  1758  ralimdaa  2560  reuss2  3440  finds2  4634  ssrel  4748  ssrel2  4750  ssrelrel  4760  funfvima2  5792  tfrlem1  6363  tfrlemi1  6387  tfr1onlemaccex  6403  tfrcllemaccex  6416  tfri3  6422  nneneq  6915  ac6sfi  6956  nnnninfeq  7189  nnnninfeq2  7190  pitonn  7910  nnaddcl  9004  nnmulcl  9005  zaddcllempos  9357  zaddcllemneg  9359  peano5uzti  9428  uzind2  9432  fzind  9435  zindd  9438  uzaddcl  9654  exfzdc  10310  frec2uzltd  10477  frecuzrdgg  10490  seq3val  10534  seqvalcd  10535  seq3clss  10545  monoord  10559  seq3caopr3  10565  seqcaopr3g  10566  seq3f1olemp  10589  seqf1oglem2a  10592  seqf1og  10595  seq3id3  10598  seq3homo  10601  seq3z  10602  seqfeq4g  10605  ser3ge0  10610  exp3vallem  10614  expcllem  10624  expap0  10643  mulexp  10652  expadd  10655  expmul  10658  leexp2r  10667  leexp1a  10668  bernneq  10734  modqexp  10740  nn0ltexp2  10783  apexp1  10792  facdiv  10812  facwordi  10814  faclbnd  10815  faclbnd6  10818  omgadd  10876  seq3coll  10916  cjexp  11040  resqrexlemover  11157  resqrexlemdecn  11159  resqrexlemlo  11160  resqrexlemcalc3  11163  absexp  11226  fsum2d  11581  modfsummod  11604  fsumabs  11611  fsumiun  11623  binom  11630  bcxmas  11635  cvgratnnlemnexp  11670  cvgratnnlemmn  11671  clim2prod  11685  prodfap0  11691  prodfrecap  11692  fprodabs  11762  fprod2d  11769  demoivreALT  11920  dvdsfac  12005  gcdmultiple  12160  rplpwr  12167  nn0seqcvgd  12182  alginv  12188  algcvga  12192  algfx  12193  prmdvdsexp  12289  prmfac1  12293  eulerthlemrprm  12370  eulerthlema  12371  pcmpt  12484  pcfac  12491  prmpwdvds  12496  ennnfoneleminc  12571  ennnfonelemkh  12572  ennnfonelemhf1o  12573  ennnfonelemhom  12575  nninfdclemlt  12611  gsumfzz  13070  mulgnnass  13230  mhmmulg  13236  gsumfzconst  13414  srgmulgass  13488  srgpcomp  13489  lmodvsmmulgdi  13822  cnfldexp  14076  gsumfzfsumlemm  14086  tgcl  14243  dvmptfsum  14904  plycolemc  14936  lgsquad2lem2  15239  nninfsellemdc  15570