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  7655  curry1  8105  fsuppunfi  9362  oiid  9517  cantnflt  9655  oemapvali  9667  cnfcom2lem  9684  cfeq0  10262  recmulnq  10977  addgt0sr  11117  mappsrpr  11121  isercolllem2  15757  dvdsaddre2b  16403  ndvdssub  16505  lcmfunsn  16740  imasvscafn  17629  subcidcl  17939  funcoppc  17970  clatleglb  18612  sgrpidmnd  18847  conjsubgen  19384  gagrpid  19427  gaass  19430  cntzssv  19461  cntzi  19462  efgredlemf  19874  abveq0  20990  abvmul  20993  abvtri  20994  cnpimaex  23487  restnlly  23714  fclsopni  24247  xmeteq0  24570  xmettri2  24572  metcnpi  24776  metcnpi2  24777  causs  25532  dvbssntr  26134  dgrlem  26462  dgrlb  26469  precsexlem11  28490  umgredgne  29610  nbgrcl  29803  wlkdlem3  30150  subgrwlk  30156  usgr2trlncrct  30282  wwlksonvtx  30331  wwlksnextproplem3  30387  erclwwlknsym  30548  erclwwlkntr  30549  1pthon2v  30641  cycpmco2lem3  33576  idomsubr  33758  elrspunidl  33864  sseqf  34911  acycgrsubgr  35745  fvineqsneu  38173  pr2el2  44399  rfovcnvf1od  44852  gneispaceel  44991  gneispacess  44993  clnbgrcl  48745  linindslinci  49386  2arymaptfv  49589  f1sn2g  49787  oppf1st2nd  50065  2oppf  50066