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  549  cbv1  1733  cbv1v  1735  ralimdaa  2531  reuss2  3401  finds2  4577  ssrel  4691  ssrel2  4693  ssrelrel  4703  funfvima2  5716  tfrlem1  6272  tfrlemi1  6296  tfr1onlemaccex  6312  tfrcllemaccex  6325  tfri3  6331  nneneq  6819  ac6sfi  6860  nnnninfeq  7088  nnnninfeq2  7089  pitonn  7785  nnaddcl  8873  nnmulcl  8874  zaddcllempos  9224  zaddcllemneg  9226  peano5uzti  9295  uzind2  9299  fzind  9302  zindd  9305  uzaddcl  9520  exfzdc  10171  frec2uzltd  10334  frecuzrdgg  10347  seq3val  10389  seqvalcd  10390  seq3clss  10398  monoord  10407  seq3caopr3  10412  seq3f1olemp  10433  seq3id3  10438  seq3homo  10441  seq3z  10442  ser3ge0  10448  exp3vallem  10452  expcllem  10462  expap0  10481  mulexp  10490  expadd  10493  expmul  10496  leexp2r  10505  leexp1a  10506  bernneq  10571  modqexp  10577  nn0ltexp2  10619  apexp1  10627  facdiv  10647  facwordi  10649  faclbnd  10650  faclbnd6  10653  omgadd  10711  seq3coll  10751  cjexp  10831  resqrexlemover  10948  resqrexlemdecn  10950  resqrexlemlo  10951  resqrexlemcalc3  10954  absexp  11017  fsum2d  11372  modfsummod  11395  fsumabs  11402  fsumiun  11414  binom  11421  bcxmas  11426  cvgratnnlemnexp  11461  cvgratnnlemmn  11462  clim2prod  11476  prodfap0  11482  prodfrecap  11483  fprodabs  11553  fprod2d  11560  demoivreALT  11710  dvdsfac  11794  gcdmultiple  11949  rplpwr  11956  nn0seqcvgd  11969  alginv  11975  algcvga  11979  algfx  11980  prmdvdsexp  12076  prmfac1  12080  eulerthlemrprm  12157  eulerthlema  12158  pcmpt  12269  pcfac  12276  prmpwdvds  12281  ennnfoneleminc  12340  ennnfonelemkh  12341  ennnfonelemhf1o  12342  ennnfonelemhom  12344  nninfdclemlt  12380  tgcl  12664  nninfsellemdc  13850