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  7605  curry1  8056  fsuppunfi  9303  oiid  9458  cantnflt  9593  oemapvali  9605  cnfcom2lem  9622  cfeq0  10178  recmulnq  10887  addgt0sr  11027  mappsrpr  11031  isercolllem2  15601  dvdsaddre2b  16246  ndvdssub  16348  lcmfunsn  16583  imasvscafn  17470  subcidcl  17780  funcoppc  17811  clatleglb  18453  sgrpidmnd  18676  conjsubgen  19192  gagrpid  19235  gaass  19238  cntzssv  19269  cntzi  19270  efgredlemf  19682  abveq0  20763  abvmul  20766  abvtri  20767  cnpimaex  23212  restnlly  23438  fclsopni  23971  xmeteq0  24294  xmettri2  24296  metcnpi  24500  metcnpi2  24501  causs  25266  dvbssntr  25869  dgrlem  26202  dgrlb  26209  precsexlem11  28225  umgredgne  29230  nbgrcl  29420  wlkdlem3  29768  usgr2trlncrct  29891  wwlksonvtx  29940  wwlksnextproplem3  29996  erclwwlknsym  30157  erclwwlkntr  30158  1pthon2v  30240  cycpmco2lem3  33221  idomsubr  33402  elrspunidl  33520  sseqf  34569  subgrwlk  35345  acycgrsubgr  35371  fvineqsneu  37660  pr2el2  43901  rfovcnvf1od  44354  gneispaceel  44493  gneispacess  44495  clnbgrcl  48175  linindslinci  48802  2arymaptfv  49005  f1sn2g  49204  oppf1st2nd  49484  2oppf  49485