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 196 | . . 3 ⊢ ¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | simplim 162 | . . 3 ⊢ (¬ (((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) → ¬ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) → ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)))) | |
3 | 1, 2 | ax-mp 5 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) |
4 | simplim 162 | . 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜑 → 𝜓)) | |
5 | 3, 4 | syl 17 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜑 → 𝜓)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 |
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 196 |
This theorem is referenced by: biimpi 205 bicom1 210 biimpd 218 ibd 257 pm5.74 258 pm5.501 355 bija 369 albi 1736 exbiOLD 1763 cbv2h 2257 mo2v 2465 2eu6 2546 eleq2dOLD 2674 ceqsalt 3201 vtoclgft 3227 vtoclgftOLD 3228 spcgft 3258 pm13.183 3313 reu6 3362 reu3 3363 sbciegft 3433 fv3 6116 expeq0 12752 t1t0 20962 kqfvima 21343 ufileu 21533 cvmlift2lem1 30538 btwndiff 31304 nn0prpw 31488 bj-dfbi6 31730 bj-bi3ant 31747 bj-ssbbi 31811 bj-cbv2hv 31918 bj-eumo0 32018 bj-ceqsalt0 32067 bj-ceqsalt1 32068 bj-ax9 32083 or3or 37339 bi33imp12 37717 bi23imp1 37722 bi123imp0 37723 eqsbc3rVD 38097 imbi12VD 38131 2uasbanhVD 38169 |
Copyright terms: Public domain | W3C validator |