Theorem simpl2im 504

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  caovmo  7596  curry1  8041  fsuppunfi  9334  oiid  9486  cantnflt  9617  oemapvali  9629  cnfcom2lem  9646  cfeq0  10201  recmulnq  10909  addgt0sr  11049  mappsrpr  11053  isercolllem2  15562  dvdsaddre2b  16200  ndvdssub  16302  lcmfunsn  16531  imasvscafn  17433  subcidcl  17744  funcoppc  17775  clatleglb  18421  sgrpidmnd  18575  conjsubgen  19055  gagrpid  19088  gaass  19091  cntzssv  19122  cntzi  19123  efgredlemf  19537  abveq0  20341  abvmul  20344  abvtri  20345  cnpimaex  22644  restnlly  22870  fclsopni  23403  xmeteq0  23728  xmettri2  23730  metcnpi  23937  metcnpi2  23938  causs  24699  dvbssntr  25301  dgrlem  25627  dgrlb  25634  umgredgne  28159  nbgrcl  28346  wlkdlem3  28695  usgr2trlncrct  28814  wwlksonvtx  28863  wwlksnextproplem3  28919  erclwwlknsym  29077  erclwwlkntr  29078  1pthon2v  29160  cycpmco2lem3  32047  elrspunidl  32279  sseqf  33081  subgrwlk  33813  acycgrsubgr  33839  pr2el2  41945  rfovcnvf1od  42398  gneispaceel  42537  gneispacess  42539  linindslinci  46649  2arymaptfv  46857  f1sn2g  47037