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  7626  curry1  8083  fsuppunfi  9339  oiid  9494  cantnflt  9625  oemapvali  9637  cnfcom2lem  9654  cfeq0  10209  recmulnq  10917  addgt0sr  11057  mappsrpr  11061  isercolllem2  15632  dvdsaddre2b  16277  ndvdssub  16379  lcmfunsn  16614  imasvscafn  17500  subcidcl  17806  funcoppc  17837  clatleglb  18477  sgrpidmnd  18666  conjsubgen  19183  gagrpid  19226  gaass  19229  cntzssv  19260  cntzi  19261  efgredlemf  19671  abveq0  20727  abvmul  20730  abvtri  20731  cnpimaex  23143  restnlly  23369  fclsopni  23902  xmeteq0  24226  xmettri2  24228  metcnpi  24432  metcnpi2  24433  causs  25198  dvbssntr  25801  dgrlem  26134  dgrlb  26141  precsexlem11  28119  umgredgne  29072  nbgrcl  29262  wlkdlem3  29612  usgr2trlncrct  29736  wwlksonvtx  29785  wwlksnextproplem3  29841  erclwwlknsym  29999  erclwwlkntr  30000  1pthon2v  30082  cycpmco2lem3  33085  idomsubr  33259  elrspunidl  33399  sseqf  34383  subgrwlk  35119  acycgrsubgr  35145  fvineqsneu  37399  pr2el2  43540  rfovcnvf1od  43993  gneispaceel  44132  gneispacess  44134  clnbgrcl  47822  linindslinci  48437  2arymaptfv  48640  f1sn2g  48839  oppf1st2nd  49120  2oppf  49121