Theorem simpl2im 390

Description: Implication from an eliminated conjunct implied by the antecedent. (Contributed by BJ/AV, 5-Apr-2021.)

Hypotheses

Ref	Expression
simpl2im.1	⊢ (𝜑 → (𝜓 ∧ 𝜒))
simpl2im.2	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
simpl2im	⊢ (𝜑 → 𝜃)

Proof of Theorem simpl2im

Step	Hyp	Ref	Expression
1		simpl2im.1	. 2 ⊢ (𝜑 → (𝜓 ∧ 𝜒))
2		simpr 110	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜒)
3		simpl2im.2	. 2 ⊢ (𝜒 → 𝜃)
4	1, 2, 3	3syl 17	1 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107

This theorem is used by:  rabsnif  3778  ctssdccl  7458  enumct  7462  djuen  7574  ndvdssub  12723  sgrpidmndm  13793  conjsubgen  14141  cntzssv  14161  cntzi  14163  xmeteq0  15597  xmettri2  15599  metcnpi  15753  metcnpi2  15754  dvbssntrcntop  15922  upgrm  16558  umgrpredgv  16605