Axiom ax-L4 16

Description: Axiom of Quantified Implication.

Assertion

Ref	Expression
ax-L4	⊢ (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))

Detailed syntax breakdown of Axiom ax-L4

Step	Hyp	Ref	Expression
1		wff-ph	. . . 4 wff 𝜑
2		wff-ps	. . . 4 wff 𝜓
3	1, 2	wff-imp 10	. . 3 wff (𝜑 → 𝜓)
4		objvar-x	. . 3 objvar 𝑥
5	3, 4	wff-forall 8	. 2 wff ∀𝑥(𝜑 → 𝜓)
6	1, 4	wff-forall 8	. . 3 wff ∀𝑥𝜑
7	2, 4	wff-forall 8	. . 3 wff ∀𝑥𝜓
8	6, 7	wff-imp 10	. 2 wff (∀𝑥𝜑 → ∀𝑥𝜓)
9	5, 8	wff-imp 10	1 wff (∀𝑥(𝜑 → 𝜓) → (∀𝑥𝜑 → ∀𝑥𝜓))

This axiom is referenced by:  alloverim-P5  588  qimeqallav-P5-L1  617  qimeqalla-P6-L1  698