Theorem mae-P1.1 33

Description: Middle Antecedent Elimination Inference.

Hypotheses

Ref	Expression
mae-P1.1.1	⊢ (𝜑 → (𝜓 → 𝜒))
mae-P1.1.2	⊢ 𝜓

Assertion

Ref	Expression
mae-P1.1	⊢ (𝜑 → 𝜒)

Proof of Theorem mae-P1.1

Step	Hyp	Ref	Expression
1		mae-P1.1.2	. . 3 ⊢ 𝜓
2	1	axL1.SH 30	. 2 ⊢ (𝜑 → 𝜓)
3		mae-P1.1.1	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
4	3	axL2.SH 31	. 2 ⊢ ((𝜑 → 𝜓) → (𝜑 → 𝜒))
5	2, 4	ax-MP 14	1 ⊢ (𝜑 → 𝜒)

Syntax hints:   → wff-imp 10

This theorem was proved from axioms:  ax-L1 11  ax-L2 12  ax-MP 14

This theorem is referenced by:  rae-P1.5  37  imcomm-P1.6  48