Theorem bj-mp2c 34720

Description: A double modus ponens inference. Inference associated with mpd 15. (Contributed by BJ, 24-Sep-2019.)

Hypotheses

Ref	Expression
bj-mp2c.1	⊢ 𝜑
bj-mp2c.2	⊢ (𝜑 → 𝜓)
bj-mp2c.3	⊢ (𝜑 → (𝜓 → 𝜒))

Assertion

Ref	Expression
bj-mp2c	⊢ 𝜒

Proof of Theorem bj-mp2c

Step	Hyp	Ref	Expression
1		bj-mp2c.1	. 2 ⊢ 𝜑
2		bj-mp2c.2	. . 3 ⊢ (𝜑 → 𝜓)
3	1, 2	ax-mp 5	. 2 ⊢ 𝜓
4		bj-mp2c.3	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
5	1, 3, 4	mp2 9	1 ⊢ 𝜒

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by: (None)