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 ⊢ (𝜑 → ((𝜓 → 𝜒) → (𝜓 → 𝜃)))

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  mpdd  41  imim2d  54  imim3i  61  loowoz  103  animpimp2impd  565  cbv1  1798  cbv1v  1800  ralimdaa  2616  reuss2  3513  finds2  4750  ssrel  4865  ssrel2  4867  ssrelrel  4877  funfvima2  5954  tfrlem1  6583  tfrlemi1  6607  tfr1onlemaccex  6623  tfrcllemaccex  6636  tfri3  6642  nneneq  7163  ac6sfi  7207  nnnninfeq  7475  nnnninfeq2  7476  pitonn  8222  nnaddcl  9334  nnmulcl  9335  zaddcllempos  9693  zaddcllemneg  9695  peano5uzti  9766  uzind2  9770  fzind  9773  zindd  9776  uzaddcl  10003  exfzdc  10677  frec2uzltd  10862  frecuzrdgg  10875  seq3val  10919  seqvalcd  10920  seq3clss  10930  monoord  10944  seq3caopr3  10950  seqcaopr3g  10951  seq3f1olemp  10974  seqf1oglem2a  10977  seqf1og  10980  seq3id3  10983  seq3homo  10986  seq3z  10987  seqfeq4g  10990  ser3ge0  10995  exp3vallem  10999  expcllem  11009  expap0  11028  mulexp  11037  expadd  11040  expmul  11043  leexp2r  11052  leexp1a  11053  bernneq  11120  modqexp  11126  nn0ltexp2  11170  apexp1  11179  facdiv  11199  facwordi  11201  faclbnd  11202  faclbnd6  11205  omgadd  11265  hashmap  11291  hashf1  11310  seq3coll  11317  cjexp  11681  resqrexlemover  11799  resqrexlemdecn  11801  resqrexlemlo  11802  resqrexlemcalc3  11805  absexp  11869  fsum2d  12228  modfsummod  12251  fsumabs  12258  fsumiun  12270  binom  12277  bcxmas  12282  cvgratnnlemnexp  12317  cvgratnnlemmn  12318  clim2prod  12332  prodfap0  12338  prodfrecap  12339  fprodabs  12409  fprod2d  12416  demoivreALT  12567  dvdsfac  12653  bitsinv1  12755  gcdmultiple  12823  rplpwr  12830  nn0seqcvgd  12845  alginv  12851  algcvga  12855  algfx  12856  prmdvdsexp  12953  prmfac1  12957  eulerthlemrprm  13037  eulerthlema  13038  pcmpt  13152  pcfac  13159  prmpwdvds  13164  ennnfoneleminc  13361  ennnfonelemkh  13362  ennnfonelemhf1o  13363  ennnfonelemhom  13365  nninfdclemlt  13401  mulgnnass  14020  mhmmulg  14026  gzsumconst  14234  srgmulgass  14401  srgpcomp  14402  lmodvsmmulgdi  14770  cnfldexp  15024  assamulgscm  15153  tgcl  15302  dvmptfsum  15963  plycolemc  15996  rpcxpmul2  16158  bcmono  16316  bposlem5  16327  lgsquad2lem2  16418  eupth2lemsfi  16936  eupth2fi  16937  depindlem2  16965  depindlem3  16966  nninfsellemdc  17271  nnnninfex  17283