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  7590  curry1  8044  fsuppunfi  9297  oiid  9452  cantnflt  9587  oemapvali  9599  cnfcom2lem  9616  cfeq0  10169  recmulnq  10877  addgt0sr  11017  mappsrpr  11021  isercolllem2  15591  dvdsaddre2b  16236  ndvdssub  16338  lcmfunsn  16573  imasvscafn  17459  subcidcl  17769  funcoppc  17800  clatleglb  18442  sgrpidmnd  18631  conjsubgen  19148  gagrpid  19191  gaass  19194  cntzssv  19225  cntzi  19226  efgredlemf  19638  abveq0  20721  abvmul  20724  abvtri  20725  cnpimaex  23159  restnlly  23385  fclsopni  23918  xmeteq0  24242  xmettri2  24244  metcnpi  24448  metcnpi2  24449  causs  25214  dvbssntr  25817  dgrlem  26150  dgrlb  26157  precsexlem11  28142  umgredgne  29108  nbgrcl  29298  wlkdlem3  29646  usgr2trlncrct  29769  wwlksonvtx  29818  wwlksnextproplem3  29874  erclwwlknsym  30032  erclwwlkntr  30033  1pthon2v  30115  cycpmco2lem3  33083  idomsubr  33258  elrspunidl  33375  sseqf  34359  subgrwlk  35104  acycgrsubgr  35130  fvineqsneu  37384  pr2el2  43524  rfovcnvf1od  43977  gneispaceel  44116  gneispacess  44118  clnbgrcl  47806  linindslinci  48434  2arymaptfv  48637  f1sn2g  48836  oppf1st2nd  49117  2oppf  49118