Theorem simpl2im 513

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  caovmo  7660  curry1  8108  fsuppunfi  9358  oiid  9513  cantnflt  9651  oemapvali  9663  cnfcom2lem  9680  cfeq0  10258  recmulnq  10967  addgt0sr  11107  mappsrpr  11111  isercolllem2  15743  dvdsaddre2b  16390  ndvdssub  16492  lcmfunsn  16727  imasvscafn  17616  subcidcl  17926  funcoppc  17957  clatleglb  18599  sgrpidmnd  18826  conjsubgen  19352  gagrpid  19395  gaass  19398  cntzssv  19429  cntzi  19430  efgredlemf  19842  abveq0  20958  abvmul  20961  abvtri  20962  cnpimaex  23450  restnlly  23676  fclsopni  24209  xmeteq0  24532  xmettri2  24534  metcnpi  24738  metcnpi2  24739  causs  25494  dvbssntr  26096  dgrlem  26423  dgrlb  26430  precsexlem11  28447  umgredgne  29532  nbgrcl  29722  wlkdlem3  30069  usgr2trlncrct  30192  wwlksonvtx  30241  wwlksnextproplem3  30297  erclwwlknsym  30458  erclwwlkntr  30459  1pthon2v  30541  cycpmco2lem3  33479  idomsubr  33661  elrspunidl  33767  sseqf  34814  subgrwlk  35645  acycgrsubgr  35671  fvineqsneu  38098  pr2el2  44318  rfovcnvf1od  44771  gneispaceel  44910  gneispacess  44912  clnbgrcl  48627  linindslinci  49269  2arymaptfv  49472  f1sn2g  49670  oppf1st2nd  49950  2oppf  49951