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	⊢ (    𝜑    ,    𝜓    ,    𝜒    ▶    ∀ 𝑥 𝜃    )