![]() |
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 613 pm4.72 736 con4biddc 754 con1biimdc 767 bijadc 776 pclem6 1265 exbir 1325 simplbi2comg 1332 albi 1357 exbi 1495 equsexd 1617 cbv2h 1634 sbiedh 1670 ceqsalt 2580 spcegft 2632 elab3gf 2692 euind 2728 reu6 2730 reuind 2744 sbciegft 2793 iota4 4885 fv3 5197 algcvgblem 9888 bj-notbi 10045 bj-inf2vnlem1 10095 |
Copyright terms: Public domain | W3C validator |