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 298 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) |
Colors of variables: wff set class |
Syntax hints: ∧ 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 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm4.71 386 mpbiran2 925 isset 2687 rexcom4b 2706 eueq 2850 ssrabeq 3178 a9evsep 4045 pwunim 4203 elvv 4596 elvvv 4597 resopab 4858 funfn 5148 dffn2 5269 dffn3 5278 dffn4 5346 fsn 5585 ixp0x 6613 ac6sfi 6785 fimax2gtri 6788 xrmaxiflemcom 11011 |
Copyright terms: Public domain | W3C validator |