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  1759  cbv1v  1761  ralimdaa  2563  reuss2  3444  finds2  4638  ssrel  4752  ssrel2  4754  ssrelrel  4764  funfvima2  5798  tfrlem1  6375  tfrlemi1  6399  tfr1onlemaccex  6415  tfrcllemaccex  6428  tfri3  6434  nneneq  6927  ac6sfi  6968  nnnninfeq  7203  nnnninfeq2  7204  pitonn  7934  nnaddcl  9029  nnmulcl  9030  zaddcllempos  9382  zaddcllemneg  9384  peano5uzti  9453  uzind2  9457  fzind  9460  zindd  9463  uzaddcl  9679  exfzdc  10335  frec2uzltd  10514  frecuzrdgg  10527  seq3val  10571  seqvalcd  10572  seq3clss  10582  monoord  10596  seq3caopr3  10602  seqcaopr3g  10603  seq3f1olemp  10626  seqf1oglem2a  10629  seqf1og  10632  seq3id3  10635  seq3homo  10638  seq3z  10639  seqfeq4g  10642  ser3ge0  10647  exp3vallem  10651  expcllem  10661  expap0  10680  mulexp  10689  expadd  10692  expmul  10695  leexp2r  10704  leexp1a  10705  bernneq  10771  modqexp  10777  nn0ltexp2  10820  apexp1  10829  facdiv  10849  facwordi  10851  faclbnd  10852  faclbnd6  10855  omgadd  10913  seq3coll  10953  cjexp  11077  resqrexlemover  11194  resqrexlemdecn  11196  resqrexlemlo  11197  resqrexlemcalc3  11200  absexp  11263  fsum2d  11619  modfsummod  11642  fsumabs  11649  fsumiun  11661  binom  11668  bcxmas  11673  cvgratnnlemnexp  11708  cvgratnnlemmn  11709  clim2prod  11723  prodfap0  11729  prodfrecap  11730  fprodabs  11800  fprod2d  11807  demoivreALT  11958  dvdsfac  12044  bitsinv1  12146  gcdmultiple  12214  rplpwr  12221  nn0seqcvgd  12236  alginv  12242  algcvga  12246  algfx  12247  prmdvdsexp  12343  prmfac1  12347  eulerthlemrprm  12424  eulerthlema  12425  pcmpt  12539  pcfac  12546  prmpwdvds  12551  ennnfoneleminc  12655  ennnfonelemkh  12656  ennnfonelemhf1o  12657  ennnfonelemhom  12659  nninfdclemlt  12695  gsumfzz  13199  mulgnnass  13365  mhmmulg  13371  gsumfzconst  13549  srgmulgass  13623  srgpcomp  13624  lmodvsmmulgdi  13957  cnfldexp  14211  gsumfzfsumlemm  14221  tgcl  14408  dvmptfsum  15069  plycolemc  15102  rpcxpmul2  15257  lgsquad2lem2  15431  nninfsellemdc  15765  nnnninfex  15777