![]() |
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 206 | . . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | simplim 167 | . . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) |
4 | simplim 167 | . 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓)) | |
5 | 3, 4 | syl 17 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 |
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 206 |
This theorem is referenced by: biimpi 215 bicom1 220 biimpd 228 ibd 269 pm5.74 270 pm5.501 367 bija 382 albi 1821 spsbbi 2077 cbv2w 2334 cbv2 2402 cbv2h 2405 dfmoeu 2531 2eu6 2653 ax9ALT 2728 ralbi 3103 rexbi 3104 ceqsalt 3474 vtoclgft 3508 spcgft 3546 pm13.183 3619 elabgt 3625 reu6 3685 reu3 3686 sbciegft 3778 axprlem4 5382 fv3 6861 expeq0 14004 t1t0 22715 kqfvima 23097 ufileu 23286 cvmlift2lem1 33953 btwndiff 34658 nn0prpw 34841 bj-animbi 35068 bj-dfbi6 35085 bj-bi3ant 35100 bj-cbv2hv 35308 bj-moeub 35361 bj-ceqsalt0 35397 bj-ceqsalt1 35398 sticksstones3 40602 or3or 42383 bi33imp12 42860 bi23imp1 42865 bi123imp0 42866 eqsbc2VD 43210 imbi12VD 43243 2uasbanhVD 43281 nimnbi 43467 thincciso 47155 |
Copyright terms: Public domain | W3C validator |