Theorem simpl2im 513

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 501	. 2 ⊢ (𝜑 → 𝜒)
3		simpl2im.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 18	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  caovmo  7682  curry1  8142  fsuppunfi  9407  oiid  9562  cantnflt  9700  oemapvali  9712  cnfcom2lem  9729  cfeq0  10361  recmulnq  11076  addgt0sr  11216  mappsrpr  11220  isercolllem2  15862  dvdsaddre2b  16506  ndvdssub  16608  lcmfunsn  16848  imasvscafn  17738  subcidcl  18048  funcoppc  18079  clatleglb  18721  sgrpidmnd  18957  conjsubgen  19494  gagrpid  19538  gaass  19541  cntzssv  19572  cntzi  19573  efgredlemf  19985  abveq0  21105  abvmul  21108  abvtri  21109  cnpimaex  23604  restnlly  23831  fclsopni  24364  xmeteq0  24687  xmettri2  24689  metcnpi  24893  metcnpi2  24894  causs  25649  dvbssntr  26250  dgrlem  26578  dgrlb  26585  precsexlem11  28633  umgredgne  29753  nbgrcl  29946  wlkdlem3  30293  subgrwlk  30299  usgr2trlncrct  30425  wwlksonvtx  30474  wwlksnextproplem3  30530  erclwwlknsym  30691  erclwwlkntr  30692  1pthon2v  30784  cycpmco2lem3  33759  idomsubr  33941  elrspunidl  34048  sseqf  35094  acycgrsubgr  36080  rankeq1o  37110  fvineqsneu  38526  pr2el2  44744  rfovcnvf1od  45196  gneispaceel  45335  gneispacess  45337  clnbgrcl  49124  linindslinci  49765  2arymaptfv  49968  f1sn2g  50167  oppf1st2nd  50452  2oppf  50453