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  1769  cbv1v  1771  ralimdaa  2573  reuss2  3454  finds2  4653  ssrel  4767  ssrel2  4769  ssrelrel  4779  funfvima2  5824  tfrlem1  6401  tfrlemi1  6425  tfr1onlemaccex  6441  tfrcllemaccex  6454  tfri3  6460  nneneq  6961  ac6sfi  7002  nnnninfeq  7237  nnnninfeq2  7238  pitonn  7968  nnaddcl  9063  nnmulcl  9064  zaddcllempos  9416  zaddcllemneg  9418  peano5uzti  9488  uzind2  9492  fzind  9495  zindd  9498  uzaddcl  9714  exfzdc  10376  frec2uzltd  10555  frecuzrdgg  10568  seq3val  10612  seqvalcd  10613  seq3clss  10623  monoord  10637  seq3caopr3  10643  seqcaopr3g  10644  seq3f1olemp  10667  seqf1oglem2a  10670  seqf1og  10673  seq3id3  10676  seq3homo  10679  seq3z  10680  seqfeq4g  10683  ser3ge0  10688  exp3vallem  10692  expcllem  10702  expap0  10721  mulexp  10730  expadd  10733  expmul  10736  leexp2r  10745  leexp1a  10746  bernneq  10812  modqexp  10818  nn0ltexp2  10861  apexp1  10870  facdiv  10890  facwordi  10892  faclbnd  10893  faclbnd6  10896  omgadd  10954  seq3coll  10994  cjexp  11248  resqrexlemover  11365  resqrexlemdecn  11367  resqrexlemlo  11368  resqrexlemcalc3  11371  absexp  11434  fsum2d  11790  modfsummod  11813  fsumabs  11820  fsumiun  11832  binom  11839  bcxmas  11844  cvgratnnlemnexp  11879  cvgratnnlemmn  11880  clim2prod  11894  prodfap0  11900  prodfrecap  11901  fprodabs  11971  fprod2d  11978  demoivreALT  12129  dvdsfac  12215  bitsinv1  12317  gcdmultiple  12385  rplpwr  12392  nn0seqcvgd  12407  alginv  12413  algcvga  12417  algfx  12418  prmdvdsexp  12514  prmfac1  12518  eulerthlemrprm  12595  eulerthlema  12596  pcmpt  12710  pcfac  12717  prmpwdvds  12722  ennnfoneleminc  12826  ennnfonelemkh  12827  ennnfonelemhf1o  12828  ennnfonelemhom  12830  nninfdclemlt  12866  gsumfzz  13371  mulgnnass  13537  mhmmulg  13543  gsumfzconst  13721  srgmulgass  13795  srgpcomp  13796  lmodvsmmulgdi  14129  cnfldexp  14383  gsumfzfsumlemm  14393  tgcl  14580  dvmptfsum  15241  plycolemc  15274  rpcxpmul2  15429  lgsquad2lem2  15603  nninfsellemdc  16021  nnnninfex  16033