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  1793  cbv1v  1795  ralimdaa  2598  reuss2  3487  finds2  4699  ssrel  4814  ssrel2  4816  ssrelrel  4826  funfvima2  5887  tfrlem1  6474  tfrlemi1  6498  tfr1onlemaccex  6514  tfrcllemaccex  6527  tfri3  6533  nneneq  7043  ac6sfi  7087  nnnninfeq  7327  nnnninfeq2  7328  pitonn  8068  nnaddcl  9163  nnmulcl  9164  zaddcllempos  9516  zaddcllemneg  9518  peano5uzti  9588  uzind2  9592  fzind  9595  zindd  9598  uzaddcl  9820  exfzdc  10487  frec2uzltd  10666  frecuzrdgg  10679  seq3val  10723  seqvalcd  10724  seq3clss  10734  monoord  10748  seq3caopr3  10754  seqcaopr3g  10755  seq3f1olemp  10778  seqf1oglem2a  10781  seqf1og  10784  seq3id3  10787  seq3homo  10790  seq3z  10791  seqfeq4g  10794  ser3ge0  10799  exp3vallem  10803  expcllem  10813  expap0  10832  mulexp  10841  expadd  10844  expmul  10847  leexp2r  10856  leexp1a  10857  bernneq  10923  modqexp  10929  nn0ltexp2  10972  apexp1  10981  facdiv  11001  facwordi  11003  faclbnd  11004  faclbnd6  11007  omgadd  11066  seq3coll  11107  cjexp  11455  resqrexlemover  11572  resqrexlemdecn  11574  resqrexlemlo  11575  resqrexlemcalc3  11578  absexp  11641  fsum2d  11998  modfsummod  12021  fsumabs  12028  fsumiun  12040  binom  12047  bcxmas  12052  cvgratnnlemnexp  12087  cvgratnnlemmn  12088  clim2prod  12102  prodfap0  12108  prodfrecap  12109  fprodabs  12179  fprod2d  12186  demoivreALT  12337  dvdsfac  12423  bitsinv1  12525  gcdmultiple  12593  rplpwr  12600  nn0seqcvgd  12615  alginv  12621  algcvga  12625  algfx  12626  prmdvdsexp  12722  prmfac1  12726  eulerthlemrprm  12803  eulerthlema  12804  pcmpt  12918  pcfac  12925  prmpwdvds  12930  ennnfoneleminc  13034  ennnfonelemkh  13035  ennnfonelemhf1o  13036  ennnfonelemhom  13038  nninfdclemlt  13074  gsumfzz  13580  mulgnnass  13746  mhmmulg  13752  gsumfzconst  13930  srgmulgass  14005  srgpcomp  14006  lmodvsmmulgdi  14340  cnfldexp  14594  gsumfzfsumlemm  14604  tgcl  14791  dvmptfsum  15452  plycolemc  15485  rpcxpmul2  15640  lgsquad2lem2  15814  eupth2lemsfi  16332  eupth2fi  16333  depindlem2  16347  depindlem3  16348  nninfsellemdc  16633  nnnninfex  16645