Theorem simpl2im 512

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  caovmo  7649  curry1  8100  fsuppunfi  9349  oiid  9504  cantnflt  9642  oemapvali  9654  cnfcom2lem  9671  cfeq0  10241  recmulnq  10950  addgt0sr  11090  mappsrpr  11094  isercolllem2  15719  dvdsaddre2b  16366  ndvdssub  16468  lcmfunsn  16703  imasvscafn  17592  subcidcl  17902  funcoppc  17933  clatleglb  18575  sgrpidmnd  18798  conjsubgen  19322  gagrpid  19365  gaass  19368  cntzssv  19399  cntzi  19400  efgredlemf  19812  abveq0  20902  abvmul  20905  abvtri  20906  cnpimaex  23394  restnlly  23620  fclsopni  24153  xmeteq0  24476  xmettri2  24478  metcnpi  24682  metcnpi2  24683  causs  25438  dvbssntr  26040  dgrlem  26367  dgrlb  26374  precsexlem11  28388  umgredgne  29473  nbgrcl  29663  wlkdlem3  30010  usgr2trlncrct  30133  wwlksonvtx  30182  wwlksnextproplem3  30238  erclwwlknsym  30399  erclwwlkntr  30400  1pthon2v  30482  cycpmco2lem3  33426  idomsubr  33608  elrspunidl  33714  sseqf  34760  subgrwlk  35602  acycgrsubgr  35628  fvineqsneu  38035  pr2el2  44257  rfovcnvf1od  44710  gneispaceel  44849  gneispacess  44851  clnbgrcl  48563  linindslinci  49205  2arymaptfv  49408  f1sn2g  49606  oppf1st2nd  49886  2oppf  49887