![]() |
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 301 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜑 ∧ 𝜓))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ (𝜑 ∧ 𝜓)) |
Colors of variables: wff set class |
Syntax hints: ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: mpbiran 940 truan 1370 rexv 2755 reuv 2756 rmov 2757 rabab 2758 euxfrdc 2923 euind 2924 dfdif3 3245 ddifstab 3267 vss 3470 mptv 4100 regexmidlem1 4532 peano5 4597 intirr 5015 fvopab6 5612 riotav 5835 mpov 5964 brtpos0 6252 frec0g 6397 inl11 7063 apreim 8558 clim0 11288 gcd0id 11974 nnwosdc 12034 isbasis3g 13437 opnssneib 13549 ssidcn 13603 bj-d0clsepcl 14559 |
Copyright terms: Public domain | W3C validator |