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  7658  curry1  8117  fsuppunfi  9383  oiid  9538  cantnflt  9676  oemapvali  9688  cnfcom2lem  9705  cfeq0  10337  recmulnq  11052  addgt0sr  11192  mappsrpr  11196  isercolllem2  15838  dvdsaddre2b  16482  ndvdssub  16584  lcmfunsn  16824  imasvscafn  17714  subcidcl  18024  funcoppc  18055  clatleglb  18697  sgrpidmnd  18933  conjsubgen  19470  gagrpid  19513  gaass  19516  cntzssv  19547  cntzi  19548  efgredlemf  19960  abveq0  21080  abvmul  21083  abvtri  21084  cnpimaex  23579  restnlly  23806  fclsopni  24339  xmeteq0  24662  xmettri2  24664  metcnpi  24868  metcnpi2  24869  causs  25624  dvbssntr  26225  dgrlem  26553  dgrlb  26560  precsexlem11  28608  umgredgne  29728  nbgrcl  29921  wlkdlem3  30268  subgrwlk  30274  usgr2trlncrct  30400  wwlksonvtx  30449  wwlksnextproplem3  30505  erclwwlknsym  30666  erclwwlkntr  30667  1pthon2v  30759  cycpmco2lem3  33735  idomsubr  33917  elrspunidl  34024  sseqf  35070  acycgrsubgr  35999  rankeq1o  37024  fvineqsneu  38427  pr2el2  44645  rfovcnvf1od  45097  gneispaceel  45236  gneispacess  45238  clnbgrcl  49012  linindslinci  49653  2arymaptfv  49856  f1sn2g  50055  oppf1st2nd  50340  2oppf  50341