![]() |
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 203 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
2 | simprim 162 | . 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑)) | |
3 | 1, 2 | sylbi 207 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 196 |
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 197 |
This theorem is referenced by: bicom1 211 pm5.74 259 bija 369 simplbi2comt 657 pm4.72 956 bianir 1047 albi 1895 cbv2h 2414 equvel 2484 euex 2631 2eu6 2696 ceqsalt 3368 euind 3534 reu6 3536 reuind 3552 sbciegft 3607 axpr 5054 iota4 6030 fv3 6367 nn0prpwlem 32623 nn0prpw 32624 bj-bi3ant 32880 bj-ssbbi 32928 bj-cbv2hv 33037 bj-ceqsalt0 33179 bj-ceqsalt1 33180 dfgcd3 33481 tsbi3 34255 mapdrvallem2 37436 axc11next 39109 pm13.192 39113 exbir 39186 con5 39230 sbcim2g 39250 trsspwALT 39547 trsspwALT2 39548 sspwtr 39550 sspwtrALT 39551 pwtrVD 39558 pwtrrVD 39559 snssiALTVD 39561 sstrALT2VD 39568 sstrALT2 39569 suctrALT2VD 39570 eqsbc3rVD 39574 simplbi2VD 39580 exbirVD 39587 exbiriVD 39588 imbi12VD 39608 sbcim2gVD 39610 simplbi2comtVD 39623 con5VD 39635 2uasbanhVD 39646 |
Copyright terms: Public domain | W3C validator |