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  7637  curry1  8087  fsuppunfi  9336  oiid  9491  cantnflt  9629  oemapvali  9641  cnfcom2lem  9658  cfeq0  10228  recmulnq  10937  addgt0sr  11077  mappsrpr  11081  isercolllem2  15707  dvdsaddre2b  16355  ndvdssub  16457  lcmfunsn  16692  imasvscafn  17581  subcidcl  17891  funcoppc  17922  clatleglb  18564  sgrpidmnd  18787  conjsubgen  19312  gagrpid  19355  gaass  19358  cntzssv  19389  cntzi  19390  efgredlemf  19802  abveq0  20890  abvmul  20893  abvtri  20894  cnpimaex  23374  restnlly  23600  fclsopni  24133  xmeteq0  24456  xmettri2  24458  metcnpi  24662  metcnpi2  24663  causs  25418  dvbssntr  26020  dgrlem  26347  dgrlb  26354  precsexlem11  28368  umgredgne  29404  nbgrcl  29594  wlkdlem3  29941  usgr2trlncrct  30064  wwlksonvtx  30113  wwlksnextproplem3  30169  erclwwlknsym  30330  erclwwlkntr  30331  1pthon2v  30413  cycpmco2lem3  33361  idomsubr  33545  elrspunidl  33652  sseqf  34699  subgrwlk  35495  acycgrsubgr  35521  fvineqsneu  37917  pr2el2  44139  rfovcnvf1od  44592  gneispaceel  44731  gneispacess  44733  clnbgrcl  48441  linindslinci  49079  2arymaptfv  49282  f1sn2g  49480  oppf1st2nd  49760  2oppf  49761