Metamath Proof Explorer


Theorem exbid

Description: Formula-building rule for existential quantifier (deduction form). (Contributed by Mario Carneiro, 24-Sep-2016)

Ref Expression
Hypotheses albid.1 xφ
albid.2 φψχ
Assertion exbid φxψxχ

Proof

Step Hyp Ref Expression
1 albid.1 xφ
2 albid.2 φψχ
3 1 nf5ri φxφ
4 3 2 exbidh φxψxχ