Theorem simpl2im 502

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 494	. 2 ⊢ (𝜑 → 𝜒)
3		simpl2im.2	. 2 ⊢ (𝜒 → 𝜃)
4	2, 3	syl 17	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ wa 394

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 206  df-an 395

This theorem is referenced by:  caovmo  7658  curry1  8109  fsuppunfi  9413  oiid  9566  cantnflt  9697  oemapvali  9709  cnfcom2lem  9726  cfeq0  10281  recmulnq  10989  addgt0sr  11129  mappsrpr  11133  isercolllem2  15648  dvdsaddre2b  16287  ndvdssub  16389  lcmfunsn  16618  imasvscafn  17522  subcidcl  17833  funcoppc  17864  clatleglb  18513  sgrpidmnd  18702  conjsubgen  19214  gagrpid  19257  gaass  19260  cntzssv  19291  cntzi  19292  efgredlemf  19708  abveq0  20718  abvmul  20721  abvtri  20722  cnpimaex  23204  restnlly  23430  fclsopni  23963  xmeteq0  24288  xmettri2  24290  metcnpi  24497  metcnpi2  24498  causs  25270  dvbssntr  25873  dgrlem  26208  dgrlb  26215  precsexlem11  28165  umgredgne  29030  nbgrcl  29220  wlkdlem3  29570  usgr2trlncrct  29689  wwlksonvtx  29738  wwlksnextproplem3  29794  erclwwlknsym  29952  erclwwlkntr  29953  1pthon2v  30035  cycpmco2lem3  32941  idomsubr  33095  elrspunidl  33240  sseqf  34140  subgrwlk  34870  acycgrsubgr  34896  pr2el2  43120  rfovcnvf1od  43573  gneispaceel  43712  gneispacess  43714  clnbgrcl  47295  linindslinci  47699  2arymaptfv  47907  f1sn2g  48086