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	$$⊢\left(\phi ,\psi ,\chi \to \theta \right)$$
Assertion	gen31	$$⊢\left(\phi ,\psi ,\chi \to \forall x\theta \right)$$

Proof

Step	Hyp	Ref	Expression
1		gen31.1	$$⊢\left(\phi ,\psi ,\chi \to \theta \right)$$
2	1	dfvd3i	$$⊢\phi \to \left(\psi \to \left(\chi \to \theta \right)\right)$$
3	2	ggen31	$$⊢\phi \to \left(\psi \to \left(\chi \to \forall x\theta \right)\right)$$
4	3	dfvd3ir	$$⊢\left(\phi ,\psi ,\chi \to \forall x\theta \right)$$