Theorem simpl2im 506

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  caovmo  7387  curry1  7801  fsuppunfi  8855  oiid  9007  cantnflt  9137  oemapvali  9149  cnfcom2lem  9166  cfeq0  9680  recmulnq  10388  addgt0sr  10528  mappsrpr  10532  isercolllem2  15024  dvdsaddre2b  15659  ndvdssub  15762  lcmfunsn  15990  imasvscafn  16812  subcidcl  17116  funcoppc  17147  clatleglb  17738  sgrpidmnd  17918  conjsubgen  18393  gagrpid  18426  gaass  18429  cntzssv  18460  cntzi  18461  efgredlemf  18869  abveq0  19599  abvmul  19602  abvtri  19603  cnpimaex  21866  restnlly  22092  fclsopni  22625  xmeteq0  22950  xmettri2  22952  metcnpi  23156  metcnpi2  23157  causs  23903  dvbssntr  24500  dgrlem  24821  dgrlb  24828  umgredgne  26932  nbgrcl  27119  wlkdlem3  27468  usgr2trlncrct  27586  wwlksonvtx  27635  wwlksnextproplem3  27692  erclwwlknsym  27851  erclwwlkntr  27852  1pthon2v  27934  cycpmco2lem3  30772  sseqf  31652  subgrwlk  32381  acycgrsubgr  32407  pr2el2  39917  rfovcnvf1od  40357  gneispaceel  40500  gneispacess  40502  linindslinci  44510