Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > biimp | Structured version Visualization version GIF version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) |
Ref | Expression |
---|---|
biimp | ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 208 | . . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | simplim 168 | . . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) |
4 | simplim 168 | . 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓)) | |
5 | 3, 4 | syl 17 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 207 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 208 |
This theorem is referenced by: biimpi 217 bicom1 222 biimpd 230 ibd 270 pm5.74 271 pm5.501 368 bija 382 albi 1810 spsbbi 2069 cbv2w 2348 cbv2 2414 cbv2h 2417 dfmoeu 2611 2eu6 2737 ax9ALT 2814 ralbi 3164 ceqsalt 3525 vtoclgft 3551 vtoclgftOLD 3552 spcgft 3584 pm13.183 3656 pm13.183OLD 3657 reu6 3714 reu3 3715 sbciegft 3805 axprlem4 5317 fv3 6681 expeq0 13447 t1t0 21884 kqfvima 22266 ufileu 22455 cvmlift2lem1 32446 btwndiff 33385 nn0prpw 33568 bj-animbi 33791 bj-dfbi6 33805 bj-bi3ant 33820 bj-cbv2hv 34016 bj-moeub 34070 bj-ceqsalt0 34097 bj-ceqsalt1 34098 bj-ax9 34113 or3or 40249 bi33imp12 40701 bi23imp1 40706 bi123imp0 40707 eqsbc3rVD 41051 imbi12VD 41084 2uasbanhVD 41122 |
Copyright terms: Public domain | W3C validator |