![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bi2 | GIF version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Proof shortened by Wolf Lammen, 11-Nov-2012.) |
Ref | Expression |
---|---|
bi2 | ⊢ ((φ ↔ ψ) → (ψ → φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 110 | . . 3 ⊢ (((φ ↔ ψ) → ((φ → ψ) ∧ (ψ → φ))) ∧ (((φ → ψ) ∧ (ψ → φ)) → (φ ↔ ψ))) | |
2 | 1 | simpli 104 | . 2 ⊢ ((φ ↔ ψ) → ((φ → ψ) ∧ (ψ → φ))) |
3 | 2 | simprd 107 | 1 ⊢ ((φ ↔ ψ) → (ψ → φ)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: bicom1 122 pm5.74 168 bi3ant 213 pm5.32d 423 nbn2 612 pm4.72 735 con4biddc 753 con1biimdc 766 bijadc 775 pclem6 1264 exbir 1322 simplbi2comg 1329 albi 1354 exbi 1492 equsexd 1614 cbv2h 1631 sbiedh 1667 ceqsalt 2574 spcegft 2626 elab3gf 2686 euind 2722 reu6 2724 reuind 2738 sbciegft 2787 iota4 4828 fv3 5140 bj-notbi 9380 bj-inf2vnlem1 9430 |
Copyright terms: Public domain | W3C validator |