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  3503  finds2  4725  ssrel  4840  ssrel2  4842  ssrelrel  4852  funfvima2  5921  tfrlem1  6541  tfrlemi1  6565  tfr1onlemaccex  6581  tfrcllemaccex  6594  tfri3  6600  nneneq  7113  ac6sfi  7157  nnnninfeq  7421  nnnninfeq2  7422  pitonn  8168  nnaddcl  9262  nnmulcl  9263  zaddcllempos  9619  zaddcllemneg  9621  peano5uzti  9692  uzind2  9696  fzind  9699  zindd  9702  uzaddcl  9924  exfzdc  10593  frec2uzltd  10772  frecuzrdgg  10785  seq3val  10829  seqvalcd  10830  seq3clss  10840  monoord  10854  seq3caopr3  10860  seqcaopr3g  10861  seq3f1olemp  10884  seqf1oglem2a  10887  seqf1og  10890  seq3id3  10893  seq3homo  10896  seq3z  10897  seqfeq4g  10900  ser3ge0  10905  exp3vallem  10909  expcllem  10919  expap0  10938  mulexp  10947  expadd  10950  expmul  10953  leexp2r  10962  leexp1a  10963  bernneq  11030  modqexp  11036  nn0ltexp2  11079  apexp1  11088  facdiv  11108  facwordi  11110  faclbnd  11111  faclbnd6  11114  omgadd  11174  hashmap  11200  seq3coll  11222  cjexp  11586  resqrexlemover  11703  resqrexlemdecn  11705  resqrexlemlo  11706  resqrexlemcalc3  11709  absexp  11772  fsum2d  12129  modfsummod  12152  fsumabs  12159  fsumiun  12171  binom  12178  bcxmas  12183  cvgratnnlemnexp  12218  cvgratnnlemmn  12219  clim2prod  12233  prodfap0  12239  prodfrecap  12240  fprodabs  12310  fprod2d  12317  demoivreALT  12468  dvdsfac  12554  bitsinv1  12656  gcdmultiple  12724  rplpwr  12731  nn0seqcvgd  12746  alginv  12752  algcvga  12756  algfx  12757  prmdvdsexp  12853  prmfac1  12857  eulerthlemrprm  12934  eulerthlema  12935  pcmpt  13049  pcfac  13056  prmpwdvds  13061  ennnfoneleminc  13183  ennnfonelemkh  13184  ennnfonelemhf1o  13185  ennnfonelemhom  13187  nninfdclemlt  13223  gsumfzz  13729  mulgnnass  13895  mhmmulg  13901  gsumfzconst  14079  srgmulgass  14154  srgpcomp  14155  lmodvsmmulgdi  14520  cnfldexp  14774  gsumfzfsumlemm  14784  tgcl  14978  dvmptfsum  15639  plycolemc  15672  rpcxpmul2  15827  lgsquad2lem2  16004  eupth2lemsfi  16522  eupth2fi  16523  depindlem2  16551  depindlem3  16552  nninfsellemdc  16837  nnnninfex  16849