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  7650  curry1  8104  fsuppunfi  9364  oiid  9519  cantnflt  9657  oemapvali  9669  cnfcom2lem  9686  cfeq0  10315  recmulnq  11030  addgt0sr  11170  mappsrpr  11174  isercolllem2  15813  dvdsaddre2b  16457  ndvdssub  16559  lcmfunsn  16799  imasvscafn  17689  subcidcl  17999  funcoppc  18030  clatleglb  18672  sgrpidmnd  18908  conjsubgen  19445  gagrpid  19488  gaass  19491  cntzssv  19522  cntzi  19523  efgredlemf  19935  abveq0  21055  abvmul  21058  abvtri  21059  cnpimaex  23554  restnlly  23781  fclsopni  24314  xmeteq0  24637  xmettri2  24639  metcnpi  24843  metcnpi2  24844  causs  25599  dvbssntr  26200  dgrlem  26528  dgrlb  26535  precsexlem11  28585  umgredgne  29705  nbgrcl  29898  wlkdlem3  30245  subgrwlk  30251  usgr2trlncrct  30377  wwlksonvtx  30426  wwlksnextproplem3  30482  erclwwlknsym  30643  erclwwlkntr  30644  1pthon2v  30736  cycpmco2lem3  33671  idomsubr  33853  elrspunidl  33960  sseqf  35007  acycgrsubgr  35892  rankeq1o  36902  fvineqsneu  38302  pr2el2  44510  rfovcnvf1od  44963  gneispaceel  45102  gneispacess  45104  clnbgrcl  48863  linindslinci  49504  2arymaptfv  49707  f1sn2g  49905  oppf1st2nd  50183  2oppf  50184