![]() |
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 205 | . 2 ⊢ ((𝜑 ↔ 𝜓) ↔ ¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑))) | |
2 | simprim 164 | . 2 ⊢ (¬ ((𝜑 → 𝜓) → ¬ (𝜓 → 𝜑)) → (𝜓 → 𝜑)) | |
3 | 1, 2 | sylbi 209 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 198 |
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 199 |
This theorem is referenced by: bicom1 213 pm5.74 262 bija 372 simplbi2comt 497 pm4.72 935 bianir 1042 albi 1862 cbv2h 2365 equvel 2421 euexOLD 2628 2eu6 2686 ceqsalt 3429 euind 3604 reu6 3606 reuind 3627 sbciegft 3682 axpr 5137 iota4 6117 fv3 6464 nn0prpwlem 32905 nn0prpw 32906 bj-bi3ant 33153 bj-ssbbi 33213 bj-cbv2hv 33318 bj-ceqsalt0 33443 bj-ceqsalt1 33444 bj-bm1.3ii 33596 dfgcd3 33766 tsbi3 34559 mapdrvallem2 37794 axc11next 39555 pm13.192 39559 exbir 39631 con5 39675 sbcim2g 39691 trsspwALT 39980 trsspwALT2 39981 sspwtr 39983 sspwtrALT 39984 pwtrVD 39986 pwtrrVD 39987 snssiALTVD 39989 sstrALT2VD 39996 sstrALT2 39997 suctrALT2VD 39998 eqsbc3rVD 40002 simplbi2VD 40008 exbirVD 40015 exbiriVD 40016 imbi12VD 40035 sbcim2gVD 40037 simplbi2comtVD 40050 con5VD 40062 2uasbanhVD 40073 absnsb 42089 |
Copyright terms: Public domain | W3C validator |