Theorem simpl2im 511

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  caovmo  7629  curry1  8078  fsuppunfi  9331  oiid  9486  cantnflt  9624  oemapvali  9636  cnfcom2lem  9653  cfeq0  10210  recmulnq  10919  addgt0sr  11059  mappsrpr  11063  isercolllem2  15676  dvdsaddre2b  16324  ndvdssub  16426  lcmfunsn  16661  imasvscafn  17550  subcidcl  17860  funcoppc  17891  clatleglb  18533  sgrpidmnd  18756  conjsubgen  19274  gagrpid  19317  gaass  19320  cntzssv  19351  cntzi  19352  efgredlemf  19764  abveq0  20847  abvmul  20850  abvtri  20851  cnpimaex  23296  restnlly  23522  fclsopni  24055  xmeteq0  24378  xmettri2  24380  metcnpi  24584  metcnpi2  24585  causs  25340  dvbssntr  25942  dgrlem  26269  dgrlb  26276  precsexlem11  28287  umgredgne  29292  nbgrcl  29482  wlkdlem3  29829  usgr2trlncrct  29952  wwlksonvtx  30001  wwlksnextproplem3  30057  erclwwlknsym  30218  erclwwlkntr  30219  1pthon2v  30301  cycpmco2lem3  33269  idomsubr  33457  elrspunidl  33575  sseqf  34650  subgrwlk  35446  acycgrsubgr  35472  fvineqsneu  37869  pr2el2  44091  rfovcnvf1od  44544  gneispaceel  44683  gneispacess  44685  clnbgrcl  48407  linindslinci  49034  2arymaptfv  49237  f1sn2g  49436  oppf1st2nd  49716  2oppf  49717