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

Metamath Proof Explorer

Theorem gen31

Description: Virtual deduction generalizing rule for one quantifying variable and three virtual hypothesis. gen31 is ggen31 with virtual deductions. (Contributed by Alan Sare, 22-Jun-2012) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis gen31.1 ⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    )
Assertion gen31 (    𝜑    ,    𝜓    ,    𝜒    ▶    ∀ 𝑥 𝜃    )

Proof

Step Hyp Ref Expression
1 gen31.1 ⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    𝜃    )
2 1 dfvd3i ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → 𝜃 ) ) )
3 2 ggen31 ⊢ ( 𝜑 → ( 𝜓 → ( 𝜒 → ∀ 𝑥 𝜃 ) ) )
4 3 dfvd3ir ⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    ∀ 𝑥 𝜃    )