![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biantru | GIF version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
biantru.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
biantru | ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantru.1 | . 2 ⊢ 𝜑 | |
2 | iba 294 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ∧ 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 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm4.71 381 mpbiran2 887 isset 2625 rexcom4b 2644 eueq 2786 ssrabeq 3107 a9evsep 3961 pwunim 4113 elvv 4500 elvvv 4501 resopab 4756 funfn 5045 dffn2 5163 dffn3 5171 dffn4 5239 fsn 5469 ac6sfi 6614 fimax2gtri 6617 |
Copyright terms: Public domain | W3C validator |