Metamath Proof Explorer


Theorem bnj1171

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypotheses bnj1171.13 φ ψ B A
bnj1171.129 z w φ ψ z B w A w R z ¬ w B
Assertion bnj1171 z w φ ψ z B w B ¬ w R z

Proof

Step Hyp Ref Expression
1 bnj1171.13 φ ψ B A
2 bnj1171.129 z w φ ψ z B w A w R z ¬ w B
3 1 sseld φ ψ w B w A
4 3 pm4.71rd φ ψ w B w A w B
5 4 imbi1d φ ψ w B ¬ w R z w A w B ¬ w R z
6 impexp w A w B ¬ w R z w A w B ¬ w R z
7 5 6 bitrdi φ ψ w B ¬ w R z w A w B ¬ w R z
8 con2b w R z ¬ w B w B ¬ w R z
9 8 imbi2i w A w R z ¬ w B w A w B ¬ w R z
10 7 9 bitr4di φ ψ w B ¬ w R z w A w R z ¬ w B
11 10 anbi2d φ ψ z B w B ¬ w R z z B w A w R z ¬ w B
12 11 pm5.74i φ ψ z B w B ¬ w R z φ ψ z B w A w R z ¬ w B
13 12 albii w φ ψ z B w B ¬ w R z w φ ψ z B w A w R z ¬ w B
14 13 exbii z w φ ψ z B w B ¬ w R z z w φ ψ z B w A w R z ¬ w B
15 2 14 mpbir z w φ ψ z B w B ¬ w R z