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 206  df-an 396

This theorem is referenced by:  caovmo  7648  curry1  8094  fsuppunfi  9387  oiid  9540  cantnflt  9671  oemapvali  9683  cnfcom2lem  9700  cfeq0  10255  recmulnq  10963  addgt0sr  11103  mappsrpr  11107  isercolllem2  15617  dvdsaddre2b  16255  ndvdssub  16357  lcmfunsn  16586  imasvscafn  17488  subcidcl  17799  funcoppc  17830  clatleglb  18476  sgrpidmnd  18665  conjsubgen  19166  gagrpid  19200  gaass  19203  cntzssv  19234  cntzi  19235  efgredlemf  19651  abveq0  20578  abvmul  20581  abvtri  20582  cnpimaex  22981  restnlly  23207  fclsopni  23740  xmeteq0  24065  xmettri2  24067  metcnpi  24274  metcnpi2  24275  causs  25047  dvbssntr  25650  dgrlem  25979  dgrlb  25986  precsexlem11  27903  umgredgne  28673  nbgrcl  28860  wlkdlem3  29209  usgr2trlncrct  29328  wwlksonvtx  29377  wwlksnextproplem3  29433  erclwwlknsym  29591  erclwwlkntr  29592  1pthon2v  29674  cycpmco2lem3  32558  elrspunidl  32821  sseqf  33690  subgrwlk  34422  acycgrsubgr  34448  pr2el2  42605  rfovcnvf1od  43058  gneispaceel  43197  gneispacess  43199  linindslinci  47217  2arymaptfv  47425  f1sn2g  47605