Theorem simpl2im 502

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

Syntax hints:   → wi 4   ∧ wa 394

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 395

This theorem is referenced by:  caovmo  7656  curry1  8107  fsuppunfi  9411  oiid  9564  cantnflt  9695  oemapvali  9707  cnfcom2lem  9724  cfeq0  10279  recmulnq  10987  addgt0sr  11127  mappsrpr  11131  isercolllem2  15644  dvdsaddre2b  16283  ndvdssub  16385  lcmfunsn  16614  imasvscafn  17518  subcidcl  17829  funcoppc  17860  clatleglb  18509  sgrpidmnd  18698  conjsubgen  19209  gagrpid  19249  gaass  19252  cntzssv  19283  cntzi  19284  efgredlemf  19700  abveq0  20710  abvmul  20713  abvtri  20714  cnpimaex  23190  restnlly  23416  fclsopni  23949  xmeteq0  24274  xmettri2  24276  metcnpi  24483  metcnpi2  24484  causs  25256  dvbssntr  25859  dgrlem  26193  dgrlb  26200  precsexlem11  28149  umgredgne  29014  nbgrcl  29204  wlkdlem3  29554  usgr2trlncrct  29673  wwlksonvtx  29722  wwlksnextproplem3  29778  erclwwlknsym  29936  erclwwlkntr  29937  1pthon2v  30019  cycpmco2lem3  32906  idomsubr  33056  elrspunidl  33206  sseqf  34082  subgrwlk  34812  acycgrsubgr  34838  pr2el2  43046  rfovcnvf1od  43499  gneispaceel  43638  gneispacess  43640  clnbgrcl  47224  linindslinci  47628  2arymaptfv  47836  f1sn2g  48015