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 370 simplbi2comt 656 pm4.72 920 bianir 1009 albi 1746 cbv2h 2269 equvel 2347 euex 2494 2eu6 2558 ceqsalt 3228 euind 3393 reu6 3395 reuind 3411 sbciegft 3466 axpr 4905 iota4 5869 fv3 6206 nn0prpwlem 32317 nn0prpw 32318 bj-bi3ant 32574 bj-ssbbi 32622 bj-cbv2hv 32731 bj-ceqsalt0 32873 bj-ceqsalt1 32874 dfgcd3 33170 tsbi3 33942 mapdrvallem2 36934 axc11next 38607 pm13.192 38611 exbir 38684 con5 38728 sbcim2g 38748 trsspwALT 39045 trsspwALT2 39046 sspwtr 39048 sspwtrALT 39049 pwtrVD 39059 pwtrrVD 39060 snssiALTVD 39062 sstrALT2VD 39069 sstrALT2 39070 suctrALT2VD 39071 eqsbc3rVD 39075 simplbi2VD 39081 exbirVD 39088 exbiriVD 39089 imbi12VD 39109 sbcim2gVD 39111 simplbi2comtVD 39124 con5VD 39136 2uasbanhVD 39147 |
Copyright terms: Public domain | W3C validator |