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  7604  curry1  8054  fsuppunfi  9301  oiid  9456  cantnflt  9593  oemapvali  9605  cnfcom2lem  9622  cfeq0  10178  recmulnq  10887  addgt0sr  11027  mappsrpr  11031  isercolllem2  15628  dvdsaddre2b  16276  ndvdssub  16378  lcmfunsn  16613  imasvscafn  17501  subcidcl  17811  funcoppc  17842  clatleglb  18484  sgrpidmnd  18707  conjsubgen  19226  gagrpid  19269  gaass  19272  cntzssv  19303  cntzi  19304  efgredlemf  19716  abveq0  20795  abvmul  20798  abvtri  20799  cnpimaex  23221  restnlly  23447  fclsopni  23980  xmeteq0  24303  xmettri2  24305  metcnpi  24509  metcnpi2  24510  causs  25265  dvbssntr  25867  dgrlem  26194  dgrlb  26201  precsexlem11  28209  umgredgne  29214  nbgrcl  29404  wlkdlem3  29751  usgr2trlncrct  29874  wwlksonvtx  29923  wwlksnextproplem3  29979  erclwwlknsym  30140  erclwwlkntr  30141  1pthon2v  30223  cycpmco2lem3  33189  idomsubr  33370  elrspunidl  33488  sseqf  34536  subgrwlk  35314  acycgrsubgr  35340  fvineqsneu  37727  pr2el2  43978  rfovcnvf1od  44431  gneispaceel  44570  gneispacess  44572  clnbgrcl  48297  linindslinci  48924  2arymaptfv  49127  f1sn2g  49326  oppf1st2nd  49606  2oppf  49607