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  102  animpimp2impd  549  cbv1  1725  cbv1v  1727  ralimdaa  2523  reuss2  3388  finds2  4562  ssrel  4676  ssrel2  4678  ssrelrel  4688  funfvima2  5701  tfrlem1  6257  tfrlemi1  6281  tfr1onlemaccex  6297  tfrcllemaccex  6310  tfri3  6316  nneneq  6804  ac6sfi  6845  nnnninfeq  7073  nnnninfeq2  7074  pitonn  7770  nnaddcl  8858  nnmulcl  8859  zaddcllempos  9209  zaddcllemneg  9211  peano5uzti  9277  uzind2  9281  fzind  9284  zindd  9287  uzaddcl  9502  exfzdc  10148  frec2uzltd  10311  frecuzrdgg  10324  seq3val  10366  seqvalcd  10367  seq3clss  10375  monoord  10384  seq3caopr3  10389  seq3f1olemp  10410  seq3id3  10415  seq3homo  10418  seq3z  10419  ser3ge0  10425  exp3vallem  10429  expcllem  10439  expap0  10458  mulexp  10467  expadd  10470  expmul  10473  leexp2r  10482  leexp1a  10483  bernneq  10547  modqexp  10553  nn0ltexp2  10595  apexp1  10603  facdiv  10623  facwordi  10625  faclbnd  10626  faclbnd6  10629  omgadd  10687  seq3coll  10724  cjexp  10804  resqrexlemover  10921  resqrexlemdecn  10923  resqrexlemlo  10924  resqrexlemcalc3  10927  absexp  10990  fsum2d  11343  modfsummod  11366  fsumabs  11373  fsumiun  11385  binom  11392  bcxmas  11397  cvgratnnlemnexp  11432  cvgratnnlemmn  11433  clim2prod  11447  prodfap0  11453  prodfrecap  11454  fprodabs  11524  fprod2d  11531  demoivreALT  11681  dvdsfac  11764  gcdmultiple  11919  rplpwr  11926  nn0seqcvgd  11933  alginv  11939  algcvga  11943  algfx  11944  prmdvdsexp  12038  prmfac1  12042  eulerthlemrprm  12119  eulerthlema  12120  ennnfoneleminc  12210  ennnfonelemkh  12211  ennnfonelemhf1o  12212  ennnfonelemhom  12214  nninfdclemlt  12252  tgcl  12534  nninfsellemdc  13653