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  7670  curry1  8128  fsuppunfi  9426  oiid  9579  cantnflt  9710  oemapvali  9722  cnfcom2lem  9739  cfeq0  10294  recmulnq  11002  addgt0sr  11142  mappsrpr  11146  isercolllem2  15699  dvdsaddre2b  16341  ndvdssub  16443  lcmfunsn  16678  imasvscafn  17584  subcidcl  17895  funcoppc  17926  clatleglb  18576  sgrpidmnd  18765  conjsubgen  19282  gagrpid  19325  gaass  19328  cntzssv  19359  cntzi  19360  efgredlemf  19774  abveq0  20836  abvmul  20839  abvtri  20840  cnpimaex  23280  restnlly  23506  fclsopni  24039  xmeteq0  24364  xmettri2  24366  metcnpi  24573  metcnpi2  24574  causs  25346  dvbssntr  25950  dgrlem  26283  dgrlb  26290  precsexlem11  28256  umgredgne  29177  nbgrcl  29367  wlkdlem3  29717  usgr2trlncrct  29836  wwlksonvtx  29885  wwlksnextproplem3  29941  erclwwlknsym  30099  erclwwlkntr  30100  1pthon2v  30182  cycpmco2lem3  33131  idomsubr  33291  elrspunidl  33436  sseqf  34374  subgrwlk  35117  acycgrsubgr  35143  fvineqsneu  37394  pr2el2  43541  rfovcnvf1od  43994  gneispaceel  44133  gneispacess  44135  clnbgrcl  47746  linindslinci  48294  2arymaptfv  48501  f1sn2g  48681