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  8938  nnmulcl  8939  zaddcllempos  9289  zaddcllemneg  9291  peano5uzti  9360  uzind2  9364  fzind  9367  zindd  9370  uzaddcl  9585  exfzdc  10239  frec2uzltd  10402  frecuzrdgg  10415  seq3val  10457  seqvalcd  10458  seq3clss  10466  monoord  10475  seq3caopr3  10480  seq3f1olemp  10501  seq3id3  10506  seq3homo  10509  seq3z  10510  ser3ge0  10516  exp3vallem  10520  expcllem  10530  expap0  10549  mulexp  10558  expadd  10561  expmul  10564  leexp2r  10573  leexp1a  10574  bernneq  10640  modqexp  10646  nn0ltexp2  10688  apexp1  10697  facdiv  10717  facwordi  10719  faclbnd  10720  faclbnd6  10723  omgadd  10781  seq3coll  10821  cjexp  10901  resqrexlemover  11018  resqrexlemdecn  11020  resqrexlemlo  11021  resqrexlemcalc3  11024  absexp  11087  fsum2d  11442  modfsummod  11465  fsumabs  11472  fsumiun  11484  binom  11491  bcxmas  11496  cvgratnnlemnexp  11531  cvgratnnlemmn  11532  clim2prod  11546  prodfap0  11552  prodfrecap  11553  fprodabs  11623  fprod2d  11630  demoivreALT  11780  dvdsfac  11865  gcdmultiple  12020  rplpwr  12027  nn0seqcvgd  12040  alginv  12046  algcvga  12050  algfx  12051  prmdvdsexp  12147  prmfac1  12151  eulerthlemrprm  12228  eulerthlema  12229  pcmpt  12340  pcfac  12347  prmpwdvds  12352  ennnfoneleminc  12411  ennnfonelemkh  12412  ennnfonelemhf1o  12413  ennnfonelemhom  12415  nninfdclemlt  12451  mulgnnass  13016  mhmmulg  13022  srgmulgass  13170  srgpcomp  13171  cnfldexp  13441  tgcl  13534  nninfsellemdc  14729