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  7687  curry1  8145  fsuppunfi  9457  oiid  9610  cantnflt  9741  oemapvali  9753  cnfcom2lem  9770  cfeq0  10325  recmulnq  11033  addgt0sr  11173  mappsrpr  11177  isercolllem2  15714  dvdsaddre2b  16355  ndvdssub  16457  lcmfunsn  16691  imasvscafn  17597  subcidcl  17908  funcoppc  17939  clatleglb  18588  sgrpidmnd  18777  conjsubgen  19291  gagrpid  19334  gaass  19337  cntzssv  19368  cntzi  19369  efgredlemf  19783  abveq0  20841  abvmul  20844  abvtri  20845  cnpimaex  23285  restnlly  23511  fclsopni  24044  xmeteq0  24369  xmettri2  24371  metcnpi  24578  metcnpi2  24579  causs  25351  dvbssntr  25955  dgrlem  26288  dgrlb  26295  precsexlem11  28259  umgredgne  29180  nbgrcl  29370  wlkdlem3  29720  usgr2trlncrct  29839  wwlksonvtx  29888  wwlksnextproplem3  29944  erclwwlknsym  30102  erclwwlkntr  30103  1pthon2v  30185  cycpmco2lem3  33121  idomsubr  33276  elrspunidl  33421  sseqf  34357  subgrwlk  35100  acycgrsubgr  35126  fvineqsneu  37377  pr2el2  43513  rfovcnvf1od  43966  gneispaceel  44105  gneispacess  44107  clnbgrcl  47695  linindslinci  48177  2arymaptfv  48385  f1sn2g  48564