Metamath Proof Explorer


Theorem dedlema

Description: Lemma for weak deduction theorem. See also ifptru . (Contributed by NM, 26-Jun-2002) (Proof shortened by Andrew Salmon, 7-May-2011)

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

Proof

Step Hyp Ref Expression
1 orc
 |-  ( ( ps /\ ph ) -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) )
2 1 expcom
 |-  ( ph -> ( ps -> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )
3 simpl
 |-  ( ( ps /\ ph ) -> ps )
4 3 a1i
 |-  ( ph -> ( ( ps /\ ph ) -> ps ) )
5 pm2.24
 |-  ( ph -> ( -. ph -> ps ) )
6 5 adantld
 |-  ( ph -> ( ( ch /\ -. ph ) -> ps ) )
7 4 6 jaod
 |-  ( ph -> ( ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) -> ps ) )
8 2 7 impbid
 |-  ( ph -> ( ps <-> ( ( ps /\ ph ) \/ ( ch /\ -. ph ) ) ) )