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 φ , ψ , χ x θ


Step Hyp Ref Expression
1 gen31.1 φ , ψ , χ θ
2 1 dfvd3i φ ψ χ θ
3 2 ggen31 φ ψ χ x θ
4 3 dfvd3ir φ , ψ , χ x θ