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  7646  curry1  8092  fsuppunfi  9385  oiid  9538  cantnflt  9669  oemapvali  9681  cnfcom2lem  9698  cfeq0  10253  recmulnq  10961  addgt0sr  11101  mappsrpr  11105  isercolllem2  15614  dvdsaddre2b  16252  ndvdssub  16354  lcmfunsn  16583  imasvscafn  17485  subcidcl  17796  funcoppc  17827  clatleglb  18473  sgrpidmnd  18632  conjsubgen  19127  gagrpid  19160  gaass  19163  cntzssv  19194  cntzi  19195  efgredlemf  19611  abveq0  20438  abvmul  20441  abvtri  20442  cnpimaex  22767  restnlly  22993  fclsopni  23526  xmeteq0  23851  xmettri2  23853  metcnpi  24060  metcnpi2  24061  causs  24822  dvbssntr  25424  dgrlem  25750  dgrlb  25757  precsexlem11  27673  umgredgne  28443  nbgrcl  28630  wlkdlem3  28979  usgr2trlncrct  29098  wwlksonvtx  29147  wwlksnextproplem3  29203  erclwwlknsym  29361  erclwwlkntr  29362  1pthon2v  29444  cycpmco2lem3  32328  elrspunidl  32591  sseqf  33460  subgrwlk  34192  acycgrsubgr  34218  pr2el2  42384  rfovcnvf1od  42837  gneispaceel  42976  gneispacess  42978  linindslinci  47207  2arymaptfv  47415  f1sn2g  47595