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  1756  cbv1v  1758  ralimdaa  2560  reuss2  3439  finds2  4633  ssrel  4747  ssrel2  4749  ssrelrel  4759  funfvima2  5791  tfrlem1  6361  tfrlemi1  6385  tfr1onlemaccex  6401  tfrcllemaccex  6414  tfri3  6420  nneneq  6913  ac6sfi  6954  nnnninfeq  7187  nnnninfeq2  7188  pitonn  7908  nnaddcl  9002  nnmulcl  9003  zaddcllempos  9354  zaddcllemneg  9356  peano5uzti  9425  uzind2  9429  fzind  9432  zindd  9435  uzaddcl  9651  exfzdc  10307  frec2uzltd  10474  frecuzrdgg  10487  seq3val  10531  seqvalcd  10532  seq3clss  10542  monoord  10556  seq3caopr3  10562  seqcaopr3g  10563  seq3f1olemp  10586  seqf1oglem2a  10589  seqf1og  10592  seq3id3  10595  seq3homo  10598  seq3z  10599  seqfeq4g  10602  ser3ge0  10607  exp3vallem  10611  expcllem  10621  expap0  10640  mulexp  10649  expadd  10652  expmul  10655  leexp2r  10664  leexp1a  10665  bernneq  10731  modqexp  10737  nn0ltexp2  10780  apexp1  10789  facdiv  10809  facwordi  10811  faclbnd  10812  faclbnd6  10815  omgadd  10873  seq3coll  10913  cjexp  11037  resqrexlemover  11154  resqrexlemdecn  11156  resqrexlemlo  11157  resqrexlemcalc3  11160  absexp  11223  fsum2d  11578  modfsummod  11601  fsumabs  11608  fsumiun  11620  binom  11627  bcxmas  11632  cvgratnnlemnexp  11667  cvgratnnlemmn  11668  clim2prod  11682  prodfap0  11688  prodfrecap  11689  fprodabs  11759  fprod2d  11766  demoivreALT  11917  dvdsfac  12002  gcdmultiple  12157  rplpwr  12164  nn0seqcvgd  12179  alginv  12185  algcvga  12189  algfx  12190  prmdvdsexp  12286  prmfac1  12290  eulerthlemrprm  12367  eulerthlema  12368  pcmpt  12481  pcfac  12488  prmpwdvds  12493  ennnfoneleminc  12568  ennnfonelemkh  12569  ennnfonelemhf1o  12570  ennnfonelemhom  12572  nninfdclemlt  12608  gsumfzz  13067  mulgnnass  13227  mhmmulg  13233  gsumfzconst  13411  srgmulgass  13485  srgpcomp  13486  lmodvsmmulgdi  13819  cnfldexp  14065  gsumfzfsumlemm  14075  tgcl  14232  nninfsellemdc  15500