Metamath Proof Explorer

Theorem ichim

Description: Formula building rule for implication in interchangeability. (Contributed by SN, 4-May-2024)

Ref Expression
Assertion ichim 
|- ( ( [ a <> b ] ph /\ [ a <> b ] ps ) -> [ a <> b ] ( ph -> ps ) )

Proof

Step Hyp Ref Expression
1 ichn 
 |-  ( [ a <> b ] ps <-> [ a <> b ] -. ps )
2 ichan 
 |-  ( ( [ a <> b ] ph /\ [ a <> b ] -. ps ) -> [ a <> b ] ( ph /\ -. ps ) )
3 1 2 sylan2b 
 |-  ( ( [ a <> b ] ph /\ [ a <> b ] ps ) -> [ a <> b ] ( ph /\ -. ps ) )
4 ichn 
 |-  ( [ a <> b ] ( ph /\ -. ps ) <-> [ a <> b ] -. ( ph /\ -. ps ) )
5 3 4 sylib 
 |-  ( ( [ a <> b ] ph /\ [ a <> b ] ps ) -> [ a <> b ] -. ( ph /\ -. ps ) )
6 iman 
 |-  ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) )
7 6 a1i 
 |-  ( T. -> ( ( ph -> ps ) <-> -. ( ph /\ -. ps ) ) )
8 7 ichbidv 
 |-  ( T. -> ( [ a <> b ] ( ph -> ps ) <-> [ a <> b ] -. ( ph /\ -. ps ) ) )
9 8 mptru 
 |-  ( [ a <> b ] ( ph -> ps ) <-> [ a <> b ] -. ( ph /\ -. ps ) )
10 5 9 sylibr 
 |-  ( ( [ a <> b ] ph /\ [ a <> b ] ps ) -> [ a <> b ] ( ph -> ps ) )