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

This theorem is referenced by:  caovmo  7597  curry1  8047  fsuppunfi  9294  oiid  9449  cantnflt  9584  oemapvali  9596  cnfcom2lem  9613  cfeq0  10169  recmulnq  10878  addgt0sr  11018  mappsrpr  11022  isercolllem2  15619  dvdsaddre2b  16267  ndvdssub  16369  lcmfunsn  16604  imasvscafn  17492  subcidcl  17802  funcoppc  17833  clatleglb  18475  sgrpidmnd  18698  conjsubgen  19217  gagrpid  19260  gaass  19263  cntzssv  19294  cntzi  19295  efgredlemf  19707  abveq0  20786  abvmul  20789  abvtri  20790  cnpimaex  23231  restnlly  23457  fclsopni  23990  xmeteq0  24313  xmettri2  24315  metcnpi  24519  metcnpi2  24520  causs  25275  dvbssntr  25877  dgrlem  26204  dgrlb  26211  precsexlem11  28223  umgredgne  29228  nbgrcl  29418  wlkdlem3  29766  usgr2trlncrct  29889  wwlksonvtx  29938  wwlksnextproplem3  29994  erclwwlknsym  30155  erclwwlkntr  30156  1pthon2v  30238  cycpmco2lem3  33204  idomsubr  33385  elrspunidl  33503  sseqf  34552  subgrwlk  35330  acycgrsubgr  35356  fvineqsneu  37741  pr2el2  43996  rfovcnvf1od  44449  gneispaceel  44588  gneispacess  44590  clnbgrcl  48309  linindslinci  48936  2arymaptfv  49139  f1sn2g  49338  oppf1st2nd  49618  2oppf  49619