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  8129  fsuppunfi  9428  oiid  9581  cantnflt  9712  oemapvali  9724  cnfcom2lem  9741  cfeq0  10296  recmulnq  11004  addgt0sr  11144  mappsrpr  11148  isercolllem2  15702  dvdsaddre2b  16344  ndvdssub  16446  lcmfunsn  16681  imasvscafn  17582  subcidcl  17889  funcoppc  17920  clatleglb  18563  sgrpidmnd  18752  conjsubgen  19269  gagrpid  19312  gaass  19315  cntzssv  19346  cntzi  19347  efgredlemf  19759  abveq0  20819  abvmul  20822  abvtri  20823  cnpimaex  23264  restnlly  23490  fclsopni  24023  xmeteq0  24348  xmettri2  24350  metcnpi  24557  metcnpi2  24558  causs  25332  dvbssntr  25935  dgrlem  26268  dgrlb  26275  precsexlem11  28241  umgredgne  29162  nbgrcl  29352  wlkdlem3  29702  usgr2trlncrct  29826  wwlksonvtx  29875  wwlksnextproplem3  29931  erclwwlknsym  30089  erclwwlkntr  30090  1pthon2v  30172  cycpmco2lem3  33148  idomsubr  33311  elrspunidl  33456  sseqf  34394  subgrwlk  35137  acycgrsubgr  35163  fvineqsneu  37412  pr2el2  43564  rfovcnvf1od  44017  gneispaceel  44156  gneispacess  44158  clnbgrcl  47808  linindslinci  48365  2arymaptfv  48572  f1sn2g  48760