Metamath Proof Explorer

Theorem con3ALT

Description: Proof of con3 from its associated inference con3i that illustrates the use of the weak deduction theorem dedt . (Contributed by NM, 27-Jun-2002) Revised to use the conditional operator. (Revised by BJ, 30-Sep-2019) Revised dedt and elimh . (Revised by Steven Nguyen, 27-Apr-2023) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion con3ALT 
|- ( ( ph -> ps ) -> ( -. ps -> -. ph ) )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ( if- ( ( ph -> ps ) , ps , ph ) <-> ps ) -> ( if- ( ( ph -> ps ) , ps , ph ) <-> ps ) )
2 1 notbid 
 |-  ( ( if- ( ( ph -> ps ) , ps , ph ) <-> ps ) -> ( -. if- ( ( ph -> ps ) , ps , ph ) <-> -. ps ) )
3 2 imbi1d 
 |-  ( ( if- ( ( ph -> ps ) , ps , ph ) <-> ps ) -> ( ( -. if- ( ( ph -> ps ) , ps , ph ) -> -. ph ) <-> ( -. ps -> -. ph ) ) )
4 imbi2 
 |-  ( ( if- ( ( ph -> ps ) , ps , ph ) <-> ps ) -> ( ( ph -> if- ( ( ph -> ps ) , ps , ph ) ) <-> ( ph -> ps ) ) )
5 imbi2 
 |-  ( ( if- ( ( ph -> ps ) , ps , ph ) <-> ph ) -> ( ( ph -> if- ( ( ph -> ps ) , ps , ph ) ) <-> ( ph -> ph ) ) )
6 id 
 |-  ( ph -> ph )
7 4 5 6 elimh 
 |-  ( ph -> if- ( ( ph -> ps ) , ps , ph ) )
8 7 con3i 
 |-  ( -. if- ( ( ph -> ps ) , ps , ph ) -> -. ph )
9 3 8 dedt 
 |-  ( ( ph -> ps ) -> ( -. ps -> -. ph ) )