| 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 213 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
| 2 | simprim 166 | . 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑)) | |
| 3 | 1, 2 | sylbi 217 | 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: bicom1 221 pm5.74 270 bija 380 simplbi2comt 501 pm4.72 951 bianir 1058 albi 1819 spsbbi 2078 cbv2w 2339 cbv2 2405 cbv2h 2408 equvel 2458 dfeumo 2534 eu6 2572 2eu6 2655 ralbi 3089 rexbi 3090 ceqsal1t 3471 elabgtOLD 3625 elabgtOLDOLD 3626 euind 3680 reu6 3682 reuind 3709 sbciegftOLD 3776 sepex 5243 axprALT 5365 axprOLD 5374 iota4 6471 fv3 6850 elirrv 9500 r1omhfb 35217 fineqvpow 35220 r1omhfbregs 35242 nn0prpwlem 36465 nn0prpw 36466 bj-animbi 36702 bj-bi3ant 36732 bj-cbv2hv 36941 bj-ceqsalt0 37028 bj-ceqsalt1 37029 bj-bm1.3ii 37208 dfgcd3 37468 tsbi3 38275 mapdrvallem2 41844 eu6w 42861 axc11next 44589 pm13.192 44593 exbir 44662 con5 44705 sbcim2g 44721 trsspwALT 45000 trsspwALT2 45001 sspwtr 45003 sspwtrALT 45004 pwtrVD 45006 pwtrrVD 45007 snssiALTVD 45009 sstrALT2VD 45016 sstrALT2 45017 suctrALT2VD 45018 eqsbc2VD 45022 simplbi2VD 45028 exbirVD 45035 exbiriVD 45036 imbi12VD 45055 sbcim2gVD 45057 simplbi2comtVD 45070 con5VD 45082 2uasbanhVD 45093 nimnbi2 45350 absnsb 47215 thincciso 49640 |
| Copyright terms: Public domain | W3C validator |