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  4748  ssrel  4863  ssrel2  4865  ssrelrel  4875  funfvima2  5951  tfrlem1  6579  tfrlemi1  6603  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfri3  6638  nneneq  7158  ac6sfi  7202  nnnninfeq  7468  nnnninfeq2  7469  pitonn  8215  nnaddcl  9325  nnmulcl  9326  zaddcllempos  9683  zaddcllemneg  9685  peano5uzti  9756  uzind2  9760  fzind  9763  zindd  9766  uzaddcl  9988  exfzdc  10661  frec2uzltd  10842  frecuzrdgg  10855  seq3val  10899  seqvalcd  10900  seq3clss  10910  monoord  10924  seq3caopr3  10930  seqcaopr3g  10931  seq3f1olemp  10954  seqf1oglem2a  10957  seqf1og  10960  seq3id3  10963  seq3homo  10966  seq3z  10967  seqfeq4g  10970  ser3ge0  10975  exp3vallem  10979  expcllem  10989  expap0  11008  mulexp  11017  expadd  11020  expmul  11023  leexp2r  11032  leexp1a  11033  bernneq  11100  modqexp  11106  nn0ltexp2  11149  apexp1  11158  facdiv  11178  facwordi  11180  faclbnd  11181  faclbnd6  11184  omgadd  11244  hashmap  11270  hashf1  11289  seq3coll  11296  cjexp  11660  resqrexlemover  11778  resqrexlemdecn  11780  resqrexlemlo  11781  resqrexlemcalc3  11784  absexp  11847  fsum2d  12204  modfsummod  12227  fsumabs  12234  fsumiun  12246  binom  12253  bcxmas  12258  cvgratnnlemnexp  12293  cvgratnnlemmn  12294  clim2prod  12308  prodfap0  12314  prodfrecap  12315  fprodabs  12385  fprod2d  12392  demoivreALT  12543  dvdsfac  12629  bitsinv1  12731  gcdmultiple  12799  rplpwr  12806  nn0seqcvgd  12821  alginv  12827  algcvga  12831  algfx  12832  prmdvdsexp  12928  prmfac1  12932  eulerthlemrprm  13009  eulerthlema  13010  pcmpt  13124  pcfac  13131  prmpwdvds  13136  ennnfoneleminc  13304  ennnfonelemkh  13305  ennnfonelemhf1o  13306  ennnfonelemhom  13308  nninfdclemlt  13344  mulgnnass  13962  mhmmulg  13968  gzsumconst  14145  srgmulgass  14295  srgpcomp  14296  lmodvsmmulgdi  14662  cnfldexp  14916  assamulgscm  15045  tgcl  15167  dvmptfsum  15828  plycolemc  15861  rpcxpmul2  16021  bcmono  16124  lgsquad2lem2  16213  eupth2lemsfi  16731  eupth2fi  16732  depindlem2  16760  depindlem3  16761  nninfsellemdc  17065  nnnninfex  17077