Metamath Proof Explorer

Theorem dedlem0b

Description: Lemma for an alternate version of weak deduction theorem. (Contributed by NM, 2-Apr-1994)

Ref Expression
Assertion dedlem0b 
|- ( -. ph -> ( ps <-> ( ( ps -> ph ) -> ( ch /\ ph ) ) ) )

Proof

Step Hyp Ref Expression
1 pm2.21 
 |-  ( -. ph -> ( ph -> ( ch /\ ph ) ) )
2 1 imim2d 
 |-  ( -. ph -> ( ( ps -> ph ) -> ( ps -> ( ch /\ ph ) ) ) )
3 2 com23 
 |-  ( -. ph -> ( ps -> ( ( ps -> ph ) -> ( ch /\ ph ) ) ) )
4 pm2.21 
 |-  ( -. ps -> ( ps -> ph ) )
5 simpr 
 |-  ( ( ch /\ ph ) -> ph )
6 4 5 imim12i 
 |-  ( ( ( ps -> ph ) -> ( ch /\ ph ) ) -> ( -. ps -> ph ) )
7 6 con1d 
 |-  ( ( ( ps -> ph ) -> ( ch /\ ph ) ) -> ( -. ph -> ps ) )
8 7 com12 
 |-  ( -. ph -> ( ( ( ps -> ph ) -> ( ch /\ ph ) ) -> ps ) )
9 3 8 impbid 
 |-  ( -. ph -> ( ps <-> ( ( ps -> ph ) -> ( ch /\ ph ) ) ) )