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

This theorem is referenced by:  caovmo  7583  curry1  8034  fsuppunfi  9272  oiid  9427  cantnflt  9562  oemapvali  9574  cnfcom2lem  9591  cfeq0  10144  recmulnq  10852  addgt0sr  10992  mappsrpr  10996  isercolllem2  15570  dvdsaddre2b  16215  ndvdssub  16317  lcmfunsn  16552  imasvscafn  17438  subcidcl  17748  funcoppc  17779  clatleglb  18421  sgrpidmnd  18644  conjsubgen  19161  gagrpid  19204  gaass  19207  cntzssv  19238  cntzi  19239  efgredlemf  19651  abveq0  20731  abvmul  20734  abvtri  20735  cnpimaex  23169  restnlly  23395  fclsopni  23928  xmeteq0  24251  xmettri2  24253  metcnpi  24457  metcnpi2  24458  causs  25223  dvbssntr  25826  dgrlem  26159  dgrlb  26166  precsexlem11  28153  umgredgne  29121  nbgrcl  29311  wlkdlem3  29659  usgr2trlncrct  29782  wwlksonvtx  29831  wwlksnextproplem3  29887  erclwwlknsym  30045  erclwwlkntr  30046  1pthon2v  30128  cycpmco2lem3  33092  idomsubr  33270  elrspunidl  33388  sseqf  34400  subgrwlk  35164  acycgrsubgr  35190  fvineqsneu  37444  pr2el2  43583  rfovcnvf1od  44036  gneispaceel  44175  gneispacess  44177  clnbgrcl  47851  linindslinci  48479  2arymaptfv  48682  f1sn2g  48881  oppf1st2nd  49162  2oppf  49163