Metamath Proof Explorer

Theorem hbntal

Description: A closed form of hbn . hbnt is another closed form of hbn . (Contributed by Alan Sare, 8-Feb-2014) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion hbntal 
|- ( A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )

Proof

Step Hyp Ref Expression
1 hba1 
 |-  ( A. x ( ph -> A. x ph ) -> A. x A. x ( ph -> A. x ph ) )
2 axc7 
 |-  ( -. A. x -. A. x ph -> ph )
3 2 con1i 
 |-  ( -. ph -> A. x -. A. x ph )
4 con3 
 |-  ( ( ph -> A. x ph ) -> ( -. A. x ph -> -. ph ) )
5 4 al2imi 
 |-  ( A. x ( ph -> A. x ph ) -> ( A. x -. A. x ph -> A. x -. ph ) )
6 3 5 syl5 
 |-  ( A. x ( ph -> A. x ph ) -> ( -. ph -> A. x -. ph ) )
7 6 alimi 
 |-  ( A. x A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )
8 1 7 syl 
 |-  ( A. x ( ph -> A. x ph ) -> A. x ( -. ph -> A. x -. ph ) )