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