Metamath Proof Explorer


Theorem 4exbidv

Description: Formula-building rule for four existential quantifiers (deduction form). (Contributed by NM, 3-Aug-1995)

Ref Expression
Hypothesis 4exbidv.1 φψχ
Assertion 4exbidv φxyzwψxyzwχ

Proof

Step Hyp Ref Expression
1 4exbidv.1 φψχ
2 1 2exbidv φzwψzwχ
3 2 2exbidv φxyzwψxyzwχ