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  7487  curry1  7915  fsuppunfi  9078  oiid  9230  cantnflt  9360  oemapvali  9372  cnfcom2lem  9389  cfeq0  9943  recmulnq  10651  addgt0sr  10791  mappsrpr  10795  isercolllem2  15305  dvdsaddre2b  15944  ndvdssub  16046  lcmfunsn  16277  imasvscafn  17165  subcidcl  17475  funcoppc  17506  clatleglb  18151  sgrpidmnd  18305  conjsubgen  18782  gagrpid  18815  gaass  18818  cntzssv  18849  cntzi  18850  efgredlemf  19262  abveq0  20001  abvmul  20004  abvtri  20005  cnpimaex  22315  restnlly  22541  fclsopni  23074  xmeteq0  23399  xmettri2  23401  metcnpi  23606  metcnpi2  23607  causs  24367  dvbssntr  24969  dgrlem  25295  dgrlb  25302  umgredgne  27418  nbgrcl  27605  wlkdlem3  27954  usgr2trlncrct  28072  wwlksonvtx  28121  wwlksnextproplem3  28177  erclwwlknsym  28335  erclwwlkntr  28336  1pthon2v  28418  cycpmco2lem3  31297  elrspunidl  31508  sseqf  32259  subgrwlk  32994  acycgrsubgr  33020  pr2el2  41047  rfovcnvf1od  41501  gneispaceel  41642  gneispacess  41644  linindslinci  45677  2arymaptfv  45885  f1sn2g  46066