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 116 | . . 3 ⊢ (((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) ∧ (((𝜑 → 𝜓) ∧ (𝜓 → 𝜑)) → (𝜑 ↔ 𝜓))) | |
2 | 1 | simpli 110 | . 2 ⊢ ((𝜑 ↔ 𝜓) → ((𝜑 → 𝜓) ∧ (𝜓 → 𝜑))) |
3 | 2 | simprd 113 | 1 ⊢ ((𝜑 ↔ 𝜓) → (𝜓 → 𝜑)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: bicom1 130 pm5.74 178 bi3ant 223 pm5.32d 445 notbi 655 nbn2 686 pm4.72 812 con4biddc 842 con1biimdc 858 bijadc 867 pclem6 1352 exbir 1412 simplbi2comg 1419 albi 1444 exbi 1583 equsexd 1707 cbv2h 1724 sbiedh 1760 ceqsalt 2712 spcegft 2765 elab3gf 2834 euind 2871 reu6 2873 reuind 2889 sbciegft 2939 iota4 5106 fv3 5444 algcvgblem 11730 bj-inf2vnlem1 13168 |
Copyright terms: Public domain | W3C validator |