This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem bnj1109

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

Ref Expression
Hypotheses bnj1109.1 
|- E. x ( ( A =/= B /\ ph ) -> ps )
bnj1109.2 
|- ( ( A = B /\ ph ) -> ps )
Assertion bnj1109 
|- E. x ( ph -> ps )

Proof

Step Hyp Ref Expression
1 bnj1109.1 
 |-  E. x ( ( A =/= B /\ ph ) -> ps )
2 bnj1109.2 
 |-  ( ( A = B /\ ph ) -> ps )
3 2 ex 
 |-  ( A = B -> ( ph -> ps ) )
4 3 a1i 
 |-  ( ( A =/= B -> ( ph -> ps ) ) -> ( A = B -> ( ph -> ps ) ) )
5 4 ax-gen 
 |-  A. x ( ( A =/= B -> ( ph -> ps ) ) -> ( A = B -> ( ph -> ps ) ) )
6 impexp 
 |-  ( ( ( A =/= B /\ ph ) -> ps ) <-> ( A =/= B -> ( ph -> ps ) ) )
7 6 exbii 
 |-  ( E. x ( ( A =/= B /\ ph ) -> ps ) <-> E. x ( A =/= B -> ( ph -> ps ) ) )
8 1 7 mpbi 
 |-  E. x ( A =/= B -> ( ph -> ps ) )
9 exintr 
 |-  ( A. x ( ( A =/= B -> ( ph -> ps ) ) -> ( A = B -> ( ph -> ps ) ) ) -> ( E. x ( A =/= B -> ( ph -> ps ) ) -> E. x ( ( A =/= B -> ( ph -> ps ) ) /\ ( A = B -> ( ph -> ps ) ) ) ) )
10 5 8 9 mp2 
 |-  E. x ( ( A =/= B -> ( ph -> ps ) ) /\ ( A = B -> ( ph -> ps ) ) )
11 exancom 
 |-  ( E. x ( ( A =/= B -> ( ph -> ps ) ) /\ ( A = B -> ( ph -> ps ) ) ) <-> E. x ( ( A = B -> ( ph -> ps ) ) /\ ( A =/= B -> ( ph -> ps ) ) ) )
12 10 11 mpbi 
 |-  E. x ( ( A = B -> ( ph -> ps ) ) /\ ( A =/= B -> ( ph -> ps ) ) )
13 df-ne 
 |-  ( A =/= B <-> -. A = B )
14 13 imbi1i 
 |-  ( ( A =/= B -> ( ph -> ps ) ) <-> ( -. A = B -> ( ph -> ps ) ) )
15 pm2.61 
 |-  ( ( A = B -> ( ph -> ps ) ) -> ( ( -. A = B -> ( ph -> ps ) ) -> ( ph -> ps ) ) )
16 15 imp 
 |-  ( ( ( A = B -> ( ph -> ps ) ) /\ ( -. A = B -> ( ph -> ps ) ) ) -> ( ph -> ps ) )
17 14 16 sylan2b 
 |-  ( ( ( A = B -> ( ph -> ps ) ) /\ ( A =/= B -> ( ph -> ps ) ) ) -> ( ph -> ps ) )
18 12 17 bnj101 
 |-  E. x ( ph -> ps )