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  1745  cbv1v  1747  ralimdaa  2543  reuss2  3415  finds2  4600  ssrel  4714  ssrel2  4716  ssrelrel  4726  funfvima2  5749  tfrlem1  6308  tfrlemi1  6332  tfr1onlemaccex  6348  tfrcllemaccex  6361  tfri3  6367  nneneq  6856  ac6sfi  6897  nnnninfeq  7125  nnnninfeq2  7126  pitonn  7846  nnaddcl  8937  nnmulcl  8938  zaddcllempos  9288  zaddcllemneg  9290  peano5uzti  9359  uzind2  9363  fzind  9366  zindd  9369  uzaddcl  9584  exfzdc  10237  frec2uzltd  10400  frecuzrdgg  10413  seq3val  10455  seqvalcd  10456  seq3clss  10464  monoord  10473  seq3caopr3  10478  seq3f1olemp  10499  seq3id3  10504  seq3homo  10507  seq3z  10508  ser3ge0  10514  exp3vallem  10518  expcllem  10528  expap0  10547  mulexp  10556  expadd  10559  expmul  10562  leexp2r  10571  leexp1a  10572  bernneq  10637  modqexp  10643  nn0ltexp2  10685  apexp1  10693  facdiv  10713  facwordi  10715  faclbnd  10716  faclbnd6  10719  omgadd  10777  seq3coll  10817  cjexp  10897  resqrexlemover  11014  resqrexlemdecn  11016  resqrexlemlo  11017  resqrexlemcalc3  11020  absexp  11083  fsum2d  11438  modfsummod  11461  fsumabs  11468  fsumiun  11480  binom  11487  bcxmas  11492  cvgratnnlemnexp  11527  cvgratnnlemmn  11528  clim2prod  11542  prodfap0  11548  prodfrecap  11549  fprodabs  11619  fprod2d  11626  demoivreALT  11776  dvdsfac  11860  gcdmultiple  12015  rplpwr  12022  nn0seqcvgd  12035  alginv  12041  algcvga  12045  algfx  12046  prmdvdsexp  12142  prmfac1  12146  eulerthlemrprm  12223  eulerthlema  12224  pcmpt  12335  pcfac  12342  prmpwdvds  12347  ennnfoneleminc  12406  ennnfonelemkh  12407  ennnfonelemhf1o  12408  ennnfonelemhom  12410  nninfdclemlt  12446  mulgnnass  12971  mhmmulg  12977  srgmulgass  13125  srgpcomp  13126  cnfldexp  13362  tgcl  13457  nninfsellemdc  14641