![]() |
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 115 | . . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | 1 | simpli 109 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
3 | 2 | simprd 112 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 102 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: bicom1 129 pm5.74 177 bi3ant 222 pm5.32d 438 nbn2 646 pm4.72 770 con4biddc 788 con1biimdc 801 bijadc 810 pclem6 1306 exbir 1366 simplbi2comg 1373 albi 1398 exbi 1536 equsexd 1658 cbv2h 1675 sbiedh 1711 ceqsalt 2626 spcegft 2678 elab3gf 2744 euind 2780 reu6 2782 reuind 2796 sbciegft 2845 iota4 4915 fv3 5229 algcvgblem 10575 bj-notbi 10874 bj-inf2vnlem1 10923 |
Copyright terms: Public domain | W3C validator |