Theorem simpl2im 508

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  caovmo  7600  curry1  8050  fsuppunfi  9298  oiid  9453  cantnflt  9591  oemapvali  9603  cnfcom2lem  9620  cfeq0  10176  recmulnq  10885  addgt0sr  11025  mappsrpr  11029  isercolllem2  15626  dvdsaddre2b  16274  ndvdssub  16376  lcmfunsn  16611  imasvscafn  17499  subcidcl  17809  funcoppc  17840  clatleglb  18482  sgrpidmnd  18705  conjsubgen  19224  gagrpid  19267  gaass  19270  cntzssv  19301  cntzi  19302  efgredlemf  19714  abveq0  20797  abvmul  20800  abvtri  20801  cnpimaex  23246  restnlly  23472  fclsopni  24005  xmeteq0  24328  xmettri2  24330  metcnpi  24534  metcnpi2  24535  causs  25290  dvbssntr  25892  dgrlem  26219  dgrlb  26226  precsexlem11  28234  umgredgne  29239  nbgrcl  29429  wlkdlem3  29776  usgr2trlncrct  29899  wwlksonvtx  29948  wwlksnextproplem3  30004  erclwwlknsym  30165  erclwwlkntr  30166  1pthon2v  30248  cycpmco2lem3  33216  idomsubr  33400  elrspunidl  33518  sseqf  34583  subgrwlk  35367  acycgrsubgr  35393  fvineqsneu  37780  pr2el2  44002  rfovcnvf1od  44455  gneispaceel  44594  gneispacess  44596  clnbgrcl  48319  linindslinci  48946  2arymaptfv  49149  f1sn2g  49348  oppf1st2nd  49628  2oppf  49629