| 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 952 bianir 1059 albi 1818 spsbbi 2073 cbv2w 2339 cbv2 2408 cbv2h 2411 equvel 2461 dfeumo 2537 eu6 2574 2eu6 2657 ralbi 3103 rexbi 3104 ceqsal1t 3514 elabgt 3672 elabgtOLD 3673 euind 3730 reu6 3732 reuind 3759 sbciegftOLD 3826 sepex 5300 axprALT 5422 axprOLD 5431 iota4 6542 fv3 6924 fineqvpow 35110 nn0prpwlem 36323 nn0prpw 36324 bj-animbi 36560 bj-bi3ant 36590 bj-cbv2hv 36798 bj-ceqsalt0 36885 bj-ceqsalt1 36886 bj-bm1.3ii 37065 dfgcd3 37325 tsbi3 38142 mapdrvallem2 41647 eu6w 42686 axc11next 44425 pm13.192 44429 exbir 44499 con5 44542 sbcim2g 44558 trsspwALT 44838 trsspwALT2 44839 sspwtr 44841 sspwtrALT 44842 pwtrVD 44844 pwtrrVD 44845 snssiALTVD 44847 sstrALT2VD 44854 sstrALT2 44855 suctrALT2VD 44856 eqsbc2VD 44860 simplbi2VD 44866 exbirVD 44873 exbiriVD 44874 imbi12VD 44893 sbcim2gVD 44895 simplbi2comtVD 44908 con5VD 44920 2uasbanhVD 44931 nimnbi2 45169 absnsb 47039 thincciso 49102 |
| Copyright terms: Public domain | W3C validator |