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  2608  reuss2  3500  finds2  4722  ssrel  4837  ssrel2  4839  ssrelrel  4849  funfvima2  5918  tfrlem1  6538  tfrlemi1  6562  tfr1onlemaccex  6578  tfrcllemaccex  6591  tfri3  6597  nneneq  7110  ac6sfi  7154  nnnninfeq  7418  nnnninfeq2  7419  pitonn  8159  nnaddcl  9253  nnmulcl  9254  zaddcllempos  9610  zaddcllemneg  9612  peano5uzti  9682  uzind2  9686  fzind  9689  zindd  9692  uzaddcl  9914  exfzdc  10582  frec2uzltd  10761  frecuzrdgg  10774  seq3val  10818  seqvalcd  10819  seq3clss  10829  monoord  10843  seq3caopr3  10849  seqcaopr3g  10850  seq3f1olemp  10873  seqf1oglem2a  10876  seqf1og  10879  seq3id3  10882  seq3homo  10885  seq3z  10886  seqfeq4g  10889  ser3ge0  10894  exp3vallem  10898  expcllem  10908  expap0  10927  mulexp  10936  expadd  10939  expmul  10942  leexp2r  10951  leexp1a  10952  bernneq  11018  modqexp  11024  nn0ltexp2  11067  apexp1  11076  facdiv  11096  facwordi  11098  faclbnd  11099  faclbnd6  11102  omgadd  11161  seq3coll  11207  cjexp  11571  resqrexlemover  11688  resqrexlemdecn  11690  resqrexlemlo  11691  resqrexlemcalc3  11694  absexp  11757  fsum2d  12114  modfsummod  12137  fsumabs  12144  fsumiun  12156  binom  12163  bcxmas  12168  cvgratnnlemnexp  12203  cvgratnnlemmn  12204  clim2prod  12218  prodfap0  12224  prodfrecap  12225  fprodabs  12295  fprod2d  12302  demoivreALT  12453  dvdsfac  12539  bitsinv1  12641  gcdmultiple  12709  rplpwr  12716  nn0seqcvgd  12731  alginv  12737  algcvga  12741  algfx  12742  prmdvdsexp  12838  prmfac1  12842  eulerthlemrprm  12919  eulerthlema  12920  pcmpt  13034  pcfac  13041  prmpwdvds  13046  ennnfoneleminc  13151  ennnfonelemkh  13152  ennnfonelemhf1o  13153  ennnfonelemhom  13155  nninfdclemlt  13191  gsumfzz  13697  mulgnnass  13863  mhmmulg  13869  gsumfzconst  14047  srgmulgass  14122  srgpcomp  14123  lmodvsmmulgdi  14458  cnfldexp  14712  gsumfzfsumlemm  14722  tgcl  14916  dvmptfsum  15577  plycolemc  15610  rpcxpmul2  15765  lgsquad2lem2  15942  eupth2lemsfi  16460  eupth2fi  16461  depindlem2  16489  depindlem3  16490  nninfsellemdc  16775  nnnninfex  16787