Theorem bj-mp2d 34648

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

Hypotheses

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

Assertion

Ref	Expression
bj-mp2d	⊢ 𝜒

Proof of Theorem bj-mp2d

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

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5

This theorem is referenced by: (None)