![]() |
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 1800 spsbbi 2051 cbv2 2379 cbv2h 2382 dfmoeu 2572 2eu6 2714 ax9ALT 2791 ralbi 3134 ceqsalt 3470 vtoclgft 3496 vtoclgftOLD 3497 spcgft 3530 pm13.183 3597 pm13.183OLD 3598 reu6 3651 reu3 3652 sbciegft 3737 axprlem4 5218 fv3 6556 expeq0 13309 t1t0 21640 kqfvima 22022 ufileu 22211 cvmlift2lem1 32158 btwndiff 33098 nn0prpw 33281 bj-animbi 33503 bj-dfbi6 33517 bj-bi3ant 33532 bj-cbv2hv 33668 bj-moeub 33747 bj-ceqsalt0 33776 bj-ceqsalt1 33777 bj-ax9 33791 or3or 39875 bi33imp12 40382 bi23imp1 40387 bi123imp0 40388 eqsbc3rVD 40732 imbi12VD 40765 2uasbanhVD 40803 |
Copyright terms: Public domain | W3C validator |