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 ) ) ) ) |
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 ) ) ) ) |