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  102  animpimp2impd  554  cbv1  1738  cbv1v  1740  ralimdaa  2536  reuss2  3407  finds2  4585  ssrel  4699  ssrel2  4701  ssrelrel  4711  funfvima2  5728  tfrlem1  6287  tfrlemi1  6311  tfr1onlemaccex  6327  tfrcllemaccex  6340  tfri3  6346  nneneq  6835  ac6sfi  6876  nnnninfeq  7104  nnnninfeq2  7105  pitonn  7810  nnaddcl  8898  nnmulcl  8899  zaddcllempos  9249  zaddcllemneg  9251  peano5uzti  9320  uzind2  9324  fzind  9327  zindd  9330  uzaddcl  9545  exfzdc  10196  frec2uzltd  10359  frecuzrdgg  10372  seq3val  10414  seqvalcd  10415  seq3clss  10423  monoord  10432  seq3caopr3  10437  seq3f1olemp  10458  seq3id3  10463  seq3homo  10466  seq3z  10467  ser3ge0  10473  exp3vallem  10477  expcllem  10487  expap0  10506  mulexp  10515  expadd  10518  expmul  10521  leexp2r  10530  leexp1a  10531  bernneq  10596  modqexp  10602  nn0ltexp2  10644  apexp1  10652  facdiv  10672  facwordi  10674  faclbnd  10675  faclbnd6  10678  omgadd  10737  seq3coll  10777  cjexp  10857  resqrexlemover  10974  resqrexlemdecn  10976  resqrexlemlo  10977  resqrexlemcalc3  10980  absexp  11043  fsum2d  11398  modfsummod  11421  fsumabs  11428  fsumiun  11440  binom  11447  bcxmas  11452  cvgratnnlemnexp  11487  cvgratnnlemmn  11488  clim2prod  11502  prodfap0  11508  prodfrecap  11509  fprodabs  11579  fprod2d  11586  demoivreALT  11736  dvdsfac  11820  gcdmultiple  11975  rplpwr  11982  nn0seqcvgd  11995  alginv  12001  algcvga  12005  algfx  12006  prmdvdsexp  12102  prmfac1  12106  eulerthlemrprm  12183  eulerthlema  12184  pcmpt  12295  pcfac  12302  prmpwdvds  12307  ennnfoneleminc  12366  ennnfonelemkh  12367  ennnfonelemhf1o  12368  ennnfonelemhom  12370  nninfdclemlt  12406  tgcl  12858  nninfsellemdc  14043