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  7629  curry1  8086  fsuppunfi  9346  oiid  9501  cantnflt  9632  oemapvali  9644  cnfcom2lem  9661  cfeq0  10216  recmulnq  10924  addgt0sr  11064  mappsrpr  11068  isercolllem2  15639  dvdsaddre2b  16284  ndvdssub  16386  lcmfunsn  16621  imasvscafn  17507  subcidcl  17813  funcoppc  17844  clatleglb  18484  sgrpidmnd  18673  conjsubgen  19190  gagrpid  19233  gaass  19236  cntzssv  19267  cntzi  19268  efgredlemf  19678  abveq0  20734  abvmul  20737  abvtri  20738  cnpimaex  23150  restnlly  23376  fclsopni  23909  xmeteq0  24233  xmettri2  24235  metcnpi  24439  metcnpi2  24440  causs  25205  dvbssntr  25808  dgrlem  26141  dgrlb  26148  precsexlem11  28126  umgredgne  29079  nbgrcl  29269  wlkdlem3  29619  usgr2trlncrct  29743  wwlksonvtx  29792  wwlksnextproplem3  29848  erclwwlknsym  30006  erclwwlkntr  30007  1pthon2v  30089  cycpmco2lem3  33092  idomsubr  33266  elrspunidl  33406  sseqf  34390  subgrwlk  35126  acycgrsubgr  35152  fvineqsneu  37406  pr2el2  43547  rfovcnvf1od  44000  gneispaceel  44139  gneispacess  44141  clnbgrcl  47826  linindslinci  48441  2arymaptfv  48644  f1sn2g  48843  oppf1st2nd  49124  2oppf  49125