![]() |
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 268 pm5.74 269 pm5.501 365 bija 379 albi 1812 spsbbi 2068 cbv2w 2327 cbv2 2396 cbv2h 2399 dfmoeu 2524 2eu6 2645 ax9ALT 2720 ralbi 3092 rexbi 3093 ceqsalt 3494 vtoclgft 3530 spcgft 3572 elabgt 3657 elabgtOLD 3658 reu6 3718 reu3 3719 sbciegftOLD 3812 axprlem4 5426 fv3 6914 expeq0 14093 t1t0 23296 kqfvima 23678 ufileu 23867 cvmlift2lem1 35043 btwndiff 35754 nn0prpw 35938 bj-animbi 36165 bj-dfbi6 36182 bj-bi3ant 36197 bj-cbv2hv 36405 bj-moeub 36457 bj-ceqsalt0 36493 bj-ceqsalt1 36494 sticksstones3 41751 eu6w 42236 or3or 43595 bi33imp12 44071 bi23imp1 44076 bi123imp0 44077 eqsbc2VD 44421 imbi12VD 44454 2uasbanhVD 44492 nimnbi 44674 thincciso 48241 |
Copyright terms: Public domain | W3C validator |