Metamath Proof Explorer

Theorem sbi1lem

Description: Lemma for sbi1 . The core of the proof was extracted from a proof of SN. (Contributed by Wolf Lammen, 5-Jun-2026)

Ref Expression
Assertion sbi1lem 
|- ( ( [ t / x ] ( ph -> ps ) /\ [ t / x ] ph ) -> A. y ( y = t -> A. x ( x = y -> ps ) ) )

Proof

Step Hyp Ref Expression
1 dfsbimp 
 |-  ( [ t / x ] ( ph -> ps ) -> A. y ( y = t -> A. x ( x = y -> ( ph -> ps ) ) ) )
2 dfsbimp 
 |-  ( [ t / x ] ph -> A. y ( y = t -> A. x ( x = y -> ph ) ) )
3 ax-2 
 |-  ( ( x = y -> ( ph -> ps ) ) -> ( ( x = y -> ph ) -> ( x = y -> ps ) ) )
4 3 al2imi 
 |-  ( A. x ( x = y -> ( ph -> ps ) ) -> ( A. x ( x = y -> ph ) -> A. x ( x = y -> ps ) ) )
5 4 imim3i 
 |-  ( ( y = t -> A. x ( x = y -> ( ph -> ps ) ) ) -> ( ( y = t -> A. x ( x = y -> ph ) ) -> ( y = t -> A. x ( x = y -> ps ) ) ) )
6 5 al2imi 
 |-  ( A. y ( y = t -> A. x ( x = y -> ( ph -> ps ) ) ) -> ( A. y ( y = t -> A. x ( x = y -> ph ) ) -> A. y ( y = t -> A. x ( x = y -> ps ) ) ) )
7 1 2 6 syl2im 
 |-  ( [ t / x ] ( ph -> ps ) -> ( [ t / x ] ph -> A. y ( y = t -> A. x ( x = y -> ps ) ) ) )
8 7 imp 
 |-  ( ( [ t / x ] ( ph -> ps ) /\ [ t / x ] ph ) -> A. y ( y = t -> A. x ( x = y -> ps ) ) )