Theorem simpl2im 507

Description: Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.) (Proof shortened by Wolf Lammen, 26-Mar-2022.)

Hypotheses

Ref	Expression
simpl2im.1	⊢ (𝜑 → (𝜓 ∧ 𝜒))
simpl2im.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
simpl2im	⊢ (𝜑 → 𝜃)

Proof of Theorem simpl2im

Step	Hyp	Ref	Expression
1		simpl2im.1	. . 3 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2	1	simprd 499	. 2 ⊢ (𝜑 → 𝜒)
3		simpl2im.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 400

This theorem is referenced by:  caovmo  7365  curry1  7782  fsuppunfi  8837  oiid  8989  cantnflt  9119  oemapvali  9131  cnfcom2lem  9148  cfeq0  9667  recmulnq  10375  addgt0sr  10515  mappsrpr  10519  isercolllem2  15014  dvdsaddre2b  15649  ndvdssub  15750  lcmfunsn  15978  imasvscafn  16802  subcidcl  17106  funcoppc  17137  clatleglb  17728  sgrpidmnd  17908  conjsubgen  18383  gagrpid  18416  gaass  18419  cntzssv  18450  cntzi  18451  efgredlemf  18859  abveq0  19590  abvmul  19593  abvtri  19594  cnpimaex  21861  restnlly  22087  fclsopni  22620  xmeteq0  22945  xmettri2  22947  metcnpi  23151  metcnpi2  23152  causs  23902  dvbssntr  24503  dgrlem  24826  dgrlb  24833  umgredgne  26938  nbgrcl  27125  wlkdlem3  27474  usgr2trlncrct  27592  wwlksonvtx  27641  wwlksnextproplem3  27697  erclwwlknsym  27855  erclwwlkntr  27856  1pthon2v  27938  cycpmco2lem3  30820  elrspunidl  31014  sseqf  31760  subgrwlk  32492  acycgrsubgr  32518  pr2el2  40250  rfovcnvf1od  40705  gneispaceel  40846  gneispacess  40848  linindslinci  44857  2arymaptfv  45065