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  7385  curry1  7799  fsuppunfi  8853  oiid  9005  cantnflt  9135  oemapvali  9147  cnfcom2lem  9164  cfeq0  9678  recmulnq  10386  addgt0sr  10526  mappsrpr  10530  isercolllem2  15022  dvdsaddre2b  15657  ndvdssub  15760  lcmfunsn  15988  imasvscafn  16810  subcidcl  17114  funcoppc  17145  clatleglb  17736  sgrpidmnd  17916  conjsubgen  18391  gagrpid  18424  gaass  18427  cntzssv  18458  cntzi  18459  efgredlemf  18867  abveq0  19597  abvmul  19600  abvtri  19601  cnpimaex  21864  restnlly  22090  fclsopni  22623  xmeteq0  22948  xmettri2  22950  metcnpi  23154  metcnpi2  23155  causs  23901  dvbssntr  24498  dgrlem  24819  dgrlb  24826  umgredgne  26930  nbgrcl  27117  wlkdlem3  27466  usgr2trlncrct  27584  wwlksonvtx  27633  wwlksnextproplem3  27690  erclwwlknsym  27849  erclwwlkntr  27850  1pthon2v  27932  cycpmco2lem3  30770  sseqf  31650  subgrwlk  32379  acycgrsubgr  32405  pr2el2  39930  rfovcnvf1od  40370  gneispaceel  40513  gneispacess  40515  linindslinci  44523