This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axc4i-o

Description: Inference version of ax-c4 . (Contributed by NM, 3-Jan-1993) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis axc4i-o.1 ⊢ ( ∀ 𝑥 𝜑 → 𝜓 )
Assertion axc4i-o ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 )

Proof

Step Hyp Ref Expression
1 axc4i-o.1 ⊢ ( ∀ 𝑥 𝜑 → 𝜓 )
2 hba1-o ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 ∀ 𝑥 𝜑 )
3 2 1 alrimih ⊢ ( ∀ 𝑥 𝜑 → ∀ 𝑥 𝜓 )