Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biantrur | GIF version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.) |
Ref | Expression |
---|---|
biantrur.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
biantrur | ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrur.1 | . 2 ⊢ 𝜑 | |
2 | ibar 285 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | ax-mp 7 | 1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 97 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: mpbiran 847 truan 1260 rexv 2572 reuv 2573 rmov 2574 rabab 2575 euxfrdc 2727 euind 2728 nssinpss 3169 nsspssun 3170 vss 3264 difsnpssim 3507 mptv 3853 regexmidlem1 4258 peano5 4321 intirr 4711 fvopab6 5264 riotav 5473 mpt2v 5594 brtpos0 5867 frec0g 5983 apreim 7594 clim0 9806 bj-d0clsepcl 10049 |
Copyright terms: Public domain | W3C validator |