| 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 207 | . . 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 206 |
| 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 207 |
| This theorem is referenced by: biimpi 216 bicom1 221 biimpd 229 ibd 269 pm5.74 270 pm5.501 366 bija 380 albi 1818 spsbbi 2073 cbv2w 2339 cbv2 2408 cbv2h 2411 dfmoeu 2536 2eu6 2657 ax9ALT 2732 ralbi 3103 rexbi 3104 ceqsalt 3515 spcgft 3549 vtoclgft 3552 elabgt 3672 elabgtOLD 3673 reu6 3732 reu3 3733 sbciegftOLD 3826 axpr 5427 axprlem4OLD 5429 fv3 6924 expeq0 14133 t1t0 23356 kqfvima 23738 ufileu 23927 axsepg2ALT 35097 cvmlift2lem1 35307 btwndiff 36028 nn0prpw 36324 bj-animbi 36560 bj-dfbi6 36576 bj-bi3ant 36590 bj-cbv2hv 36798 bj-moeub 36850 bj-ceqsalt0 36885 bj-ceqsalt1 36886 sticksstones3 42149 eu6w 42686 or3or 44036 bi33imp12 44511 bi23imp1 44515 bi123imp0 44516 eqsbc2VD 44860 imbi12VD 44893 2uasbanhVD 44931 ssclaxsep 44999 nimnbi 45168 thincciso 49102 |
| Copyright terms: Public domain | W3C validator |