Metamath Proof Explorer


Theorem bnj1101

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1101.1 x φ ψ
bnj1101.2 χ φ
Assertion bnj1101 x χ ψ

Proof

Step Hyp Ref Expression
1 bnj1101.1 x φ ψ
2 bnj1101.2 χ φ
3 pm3.42 φ ψ χ φ ψ
4 1 3 bnj101 x χ φ ψ
5 2 pm4.71i χ χ φ
6 5 imbi1i χ ψ χ φ ψ
7 6 exbii x χ ψ x χ φ ψ
8 4 7 mpbir x χ ψ