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  561  cbv1  1794  cbv1v  1796  ralimdaa  2610  reuss2  3505  finds2  4730  ssrel  4845  ssrel2  4847  ssrelrel  4857  funfvima2  5926  tfrlem1  6554  tfrlemi1  6578  tfr1onlemaccex  6594  tfrcllemaccex  6607  tfri3  6613  nneneq  7126  ac6sfi  7170  nnnninfeq  7434  nnnninfeq2  7435  pitonn  8181  nnaddcl  9279  nnmulcl  9280  zaddcllempos  9636  zaddcllemneg  9638  peano5uzti  9709  uzind2  9713  fzind  9716  zindd  9719  uzaddcl  9941  exfzdc  10613  frec2uzltd  10794  frecuzrdgg  10807  seq3val  10851  seqvalcd  10852  seq3clss  10862  monoord  10876  seq3caopr3  10882  seqcaopr3g  10883  seq3f1olemp  10906  seqf1oglem2a  10909  seqf1og  10912  seq3id3  10915  seq3homo  10918  seq3z  10919  seqfeq4g  10922  ser3ge0  10927  exp3vallem  10931  expcllem  10941  expap0  10960  mulexp  10969  expadd  10972  expmul  10975  leexp2r  10984  leexp1a  10985  bernneq  11052  modqexp  11058  nn0ltexp2  11101  apexp1  11110  facdiv  11130  facwordi  11132  faclbnd  11133  faclbnd6  11136  omgadd  11196  hashmap  11222  seq3coll  11244  cjexp  11608  resqrexlemover  11726  resqrexlemdecn  11728  resqrexlemlo  11729  resqrexlemcalc3  11732  absexp  11795  fsum2d  12152  modfsummod  12175  fsumabs  12182  fsumiun  12194  binom  12201  bcxmas  12206  cvgratnnlemnexp  12241  cvgratnnlemmn  12242  clim2prod  12256  prodfap0  12262  prodfrecap  12263  fprodabs  12333  fprod2d  12340  demoivreALT  12491  dvdsfac  12577  bitsinv1  12679  gcdmultiple  12747  rplpwr  12754  nn0seqcvgd  12769  alginv  12775  algcvga  12779  algfx  12780  prmdvdsexp  12876  prmfac1  12880  eulerthlemrprm  12957  eulerthlema  12958  pcmpt  13072  pcfac  13079  prmpwdvds  13084  ennnfoneleminc  13252  ennnfonelemkh  13253  ennnfonelemhf1o  13254  ennnfonelemhom  13256  nninfdclemlt  13292  gsumfzz  13756  mulgnnass  13916  mhmmulg  13922  gsumfzconst  14100  srgmulgass  14238  srgpcomp  14239  lmodvsmmulgdi  14603  cnfldexp  14857  gsumfzfsumlemm  14867  tgcl  15061  dvmptfsum  15722  plycolemc  15755  rpcxpmul2  15910  lgsquad2lem2  16087  eupth2lemsfi  16605  eupth2fi  16606  depindlem2  16634  depindlem3  16635  nninfsellemdc  16930  nnnninfex  16942