![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bi1 | GIF version |
Description: Property of the biconditional connective. (Contributed by NM, 11-May-1999.) (Revised by NM, 31-Jan-2015.) |
Ref | Expression |
---|---|
bi1 | ⊢ ((φ ↔ ψ) → (φ → ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-bi 110 | . . 3 ⊢ (((φ ↔ ψ) → ((φ → ψ) ∧ (ψ → φ))) ∧ (((φ → ψ) ∧ (ψ → φ)) → (φ ↔ ψ))) | |
2 | 1 | simpli 104 | . 2 ⊢ ((φ ↔ ψ) → ((φ → ψ) ∧ (ψ → φ))) |
3 | 2 | simpld 105 | 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 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: biimpi 113 bicom1 122 biimpd 132 ibd 167 pm5.74 168 bi3ant 213 pm5.501 233 pm5.32d 423 pm5.19 621 con4biddc 753 con1biimdc 766 bijadc 775 pclem6 1264 albi 1354 exbi 1492 equsexd 1614 cbv2h 1631 sbiedh 1667 eumo0 1928 ceqsalt 2574 vtoclgft 2598 spcgft 2624 pm13.183 2675 reu6 2724 reu3 2725 sbciegft 2787 fv3 5140 prnmaxl 6471 prnminu 6472 elabgft1 9252 elabgf2 9254 bj-axemptylem 9347 bj-notbi 9380 bj-inf2vn 9434 bj-inf2vn2 9435 bj-nn0sucALT 9438 |
Copyright terms: Public domain | W3C validator |