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  7577  curry1  8028  fsuppunfi  9266  oiid  9421  cantnflt  9556  oemapvali  9568  cnfcom2lem  9585  cfeq0  10138  recmulnq  10846  addgt0sr  10986  mappsrpr  10990  isercolllem2  15560  dvdsaddre2b  16205  ndvdssub  16307  lcmfunsn  16542  imasvscafn  17428  subcidcl  17738  funcoppc  17769  clatleglb  18411  sgrpidmnd  18600  conjsubgen  19117  gagrpid  19160  gaass  19163  cntzssv  19194  cntzi  19195  efgredlemf  19607  abveq0  20687  abvmul  20690  abvtri  20691  cnpimaex  23125  restnlly  23351  fclsopni  23884  xmeteq0  24207  xmettri2  24209  metcnpi  24413  metcnpi2  24414  causs  25179  dvbssntr  25782  dgrlem  26115  dgrlb  26122  precsexlem11  28109  umgredgne  29077  nbgrcl  29267  wlkdlem3  29615  usgr2trlncrct  29738  wwlksonvtx  29787  wwlksnextproplem3  29843  erclwwlknsym  30001  erclwwlkntr  30002  1pthon2v  30084  cycpmco2lem3  33065  idomsubr  33243  elrspunidl  33361  sseqf  34373  subgrwlk  35122  acycgrsubgr  35148  fvineqsneu  37402  pr2el2  43541  rfovcnvf1od  43994  gneispaceel  44133  gneispacess  44135  clnbgrcl  47819  linindslinci  48447  2arymaptfv  48650  f1sn2g  48849  oppf1st2nd  49130  2oppf  49131