Theorem simpl2im 503

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

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  caovmo  7652  curry1  8103  fsuppunfi  9403  oiid  9556  cantnflt  9687  oemapvali  9699  cnfcom2lem  9716  cfeq0  10271  recmulnq  10979  addgt0sr  11119  mappsrpr  11123  isercolllem2  15636  dvdsaddre2b  16275  ndvdssub  16377  lcmfunsn  16606  imasvscafn  17510  subcidcl  17821  funcoppc  17852  clatleglb  18501  sgrpidmnd  18690  conjsubgen  19196  gagrpid  19236  gaass  19239  cntzssv  19270  cntzi  19271  efgredlemf  19687  abveq0  20695  abvmul  20698  abvtri  20699  cnpimaex  23147  restnlly  23373  fclsopni  23906  xmeteq0  24231  xmettri2  24233  metcnpi  24440  metcnpi2  24441  causs  25213  dvbssntr  25816  dgrlem  26150  dgrlb  26157  precsexlem11  28102  umgredgne  28945  nbgrcl  29135  wlkdlem3  29485  usgr2trlncrct  29604  wwlksonvtx  29653  wwlksnextproplem3  29709  erclwwlknsym  29867  erclwwlkntr  29868  1pthon2v  29950  cycpmco2lem3  32827  elrspunidl  33079  sseqf  33948  subgrwlk  34678  acycgrsubgr  34704  pr2el2  42904  rfovcnvf1od  43357  gneispaceel  43496  gneispacess  43498  linindslinci  47439  2arymaptfv  47647  f1sn2g  47826