Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biantru | Unicode 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 387 mpbiran2 926 isset 2718 rexcom4b 2737 eueq 2883 ssrabeq 3214 a9evsep 4086 pwunim 4246 elvv 4648 elvvv 4649 resopab 4910 funfn 5200 dffn2 5321 dffn3 5330 dffn4 5398 fsn 5639 ixp0x 6671 ac6sfi 6843 fimax2gtri 6846 xrmaxiflemcom 11146 trirec0xor 13616 |
Copyright terms: Public domain | W3C validator |