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  7509  curry1  7944  fsuppunfi  9148  oiid  9300  cantnflt  9430  oemapvali  9442  cnfcom2lem  9459  cfeq0  10012  recmulnq  10720  addgt0sr  10860  mappsrpr  10864  isercolllem2  15377  dvdsaddre2b  16016  ndvdssub  16118  lcmfunsn  16349  imasvscafn  17248  subcidcl  17559  funcoppc  17590  clatleglb  18236  sgrpidmnd  18390  conjsubgen  18867  gagrpid  18900  gaass  18903  cntzssv  18934  cntzi  18935  efgredlemf  19347  abveq0  20086  abvmul  20089  abvtri  20090  cnpimaex  22407  restnlly  22633  fclsopni  23166  xmeteq0  23491  xmettri2  23493  metcnpi  23700  metcnpi2  23701  causs  24462  dvbssntr  25064  dgrlem  25390  dgrlb  25397  umgredgne  27515  nbgrcl  27702  wlkdlem3  28052  usgr2trlncrct  28171  wwlksonvtx  28220  wwlksnextproplem3  28276  erclwwlknsym  28434  erclwwlkntr  28435  1pthon2v  28517  cycpmco2lem3  31395  elrspunidl  31606  sseqf  32359  subgrwlk  33094  acycgrsubgr  33120  pr2el2  41158  rfovcnvf1od  41612  gneispaceel  41753  gneispacess  41755  linindslinci  45789  2arymaptfv  45997  f1sn2g  46178