![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > biimpr | Structured version Visualization version GIF version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
Ref | Expression |
---|---|
biimpr | ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dfbi1 212 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
2 | simprim 166 | . 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑)) | |
3 | 1, 2 | sylbi 216 | 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: bicom1 220 pm5.74 269 bija 379 simplbi2comt 500 pm4.72 947 bianir 1056 albi 1812 spsbbi 2068 cbv2w 2328 cbv2 2397 cbv2h 2400 equvel 2450 dfeumo 2526 eu6 2563 2eu6 2647 ralbi 3099 rexbi 3100 ceqsal1t 3502 elabgt 3660 elabgtOLD 3661 euind 3719 reu6 3721 reuind 3748 sbciegftOLD 3815 axprALT 5424 axpr 5430 iota4 6532 fv3 6918 fineqvpow 34721 nn0prpwlem 35811 nn0prpw 35812 bj-animbi 36039 bj-bi3ant 36071 bj-cbv2hv 36279 bj-ceqsalt0 36367 bj-ceqsalt1 36368 bj-bm1.3ii 36548 dfgcd3 36808 tsbi3 37613 mapdrvallem2 41122 axc11next 43846 pm13.192 43850 exbir 43920 con5 43964 sbcim2g 43980 trsspwALT 44260 trsspwALT2 44261 sspwtr 44263 sspwtrALT 44264 pwtrVD 44266 pwtrrVD 44267 snssiALTVD 44269 sstrALT2VD 44276 sstrALT2 44277 suctrALT2VD 44278 eqsbc2VD 44282 simplbi2VD 44288 exbirVD 44295 exbiriVD 44296 imbi12VD 44315 sbcim2gVD 44317 simplbi2comtVD 44330 con5VD 44342 2uasbanhVD 44353 nimnbi2 44539 absnsb 46411 thincciso 48106 |
Copyright terms: Public domain | W3C validator |