Theorem simpl2im 499

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

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  caovmo  7148  curry1  7550  fsuppunfi  8583  oiid  8735  cantnflt  8866  oemapvali  8878  cnfcom2lem  8895  cfeq0  9413  recmulnq  10121  addgt0sr  10261  mappsrpr  10265  isercolllem2  14804  dvdsaddre2b  15436  ndvdssub  15539  lcmfunsn  15763  imasvscafn  16583  subcidcl  16889  funcoppc  16920  clatleglb  17512  conjsubgen  18077  gagrpid  18110  gaass  18113  cntzssv  18144  cntzi  18145  efgredlemf  18539  cnpimaex  21468  nbgrcl  26682  usgr2trlncrct  27155  wwlksonvtx  27204  wwlksnextproplem3  27287  wwlksnextproplem3OLD  27288  erclwwlknsym  27468  erclwwlkntr  27469  sseqf  31053  rfovcnvf1od  39258  gneispaceel  39401  gneispacess  39403