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  565  cbv1  1798  cbv1v  1800  ralimdaa  2616  reuss2  3513  finds2  4746  ssrel  4861  ssrel2  4863  ssrelrel  4873  funfvima2  5945  tfrlem1  6573  tfrlemi1  6597  tfr1onlemaccex  6613  tfrcllemaccex  6626  tfri3  6632  nneneq  7152  ac6sfi  7196  nnnninfeq  7462  nnnninfeq2  7463  pitonn  8209  nnaddcl  9307  nnmulcl  9308  zaddcllempos  9664  zaddcllemneg  9666  peano5uzti  9737  uzind2  9741  fzind  9744  zindd  9747  uzaddcl  9969  exfzdc  10642  frec2uzltd  10823  frecuzrdgg  10836  seq3val  10880  seqvalcd  10881  seq3clss  10891  monoord  10905  seq3caopr3  10911  seqcaopr3g  10912  seq3f1olemp  10935  seqf1oglem2a  10938  seqf1og  10941  seq3id3  10944  seq3homo  10947  seq3z  10948  seqfeq4g  10951  ser3ge0  10956  exp3vallem  10960  expcllem  10970  expap0  10989  mulexp  10998  expadd  11001  expmul  11004  leexp2r  11013  leexp1a  11014  bernneq  11081  modqexp  11087  nn0ltexp2  11130  apexp1  11139  facdiv  11159  facwordi  11161  faclbnd  11162  faclbnd6  11165  omgadd  11225  hashmap  11251  hashf1  11270  seq3coll  11277  cjexp  11641  resqrexlemover  11759  resqrexlemdecn  11761  resqrexlemlo  11762  resqrexlemcalc3  11765  absexp  11828  fsum2d  12185  modfsummod  12208  fsumabs  12215  fsumiun  12227  binom  12234  bcxmas  12239  cvgratnnlemnexp  12274  cvgratnnlemmn  12275  clim2prod  12289  prodfap0  12295  prodfrecap  12296  fprodabs  12366  fprod2d  12373  demoivreALT  12524  dvdsfac  12610  bitsinv1  12712  gcdmultiple  12780  rplpwr  12787  nn0seqcvgd  12802  alginv  12808  algcvga  12812  algfx  12813  prmdvdsexp  12909  prmfac1  12913  eulerthlemrprm  12990  eulerthlema  12991  pcmpt  13105  pcfac  13112  prmpwdvds  13117  ennnfoneleminc  13285  ennnfonelemkh  13286  ennnfonelemhf1o  13287  ennnfonelemhom  13289  nninfdclemlt  13325  mulgnnass  13943  mhmmulg  13949  gzsumconst  14126  srgmulgass  14276  srgpcomp  14277  lmodvsmmulgdi  14643  cnfldexp  14897  assamulgscm  15026  tgcl  15148  dvmptfsum  15809  plycolemc  15842  rpcxpmul2  15998  lgsquad2lem2  16184  eupth2lemsfi  16702  eupth2fi  16703  depindlem2  16731  depindlem3  16732  nninfsellemdc  17027  nnnninfex  17039