![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biantrurd | GIF version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.) |
Ref | Expression |
---|---|
biantrud.1 | ⊢ (𝜑 → 𝜓) |
Ref | Expression |
---|---|
biantrurd | ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantrud.1 | . 2 ⊢ (𝜑 → 𝜓) | |
2 | ibar 296 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: 3anibar 1112 drex1 1727 elrab3t 2771 bnd2 4014 opbrop 4530 opelresi 4737 funcnv3 5089 fnssresb 5139 dff1o5 5275 fneqeql2 5422 fnniniseg2 5436 rexsupp 5437 dffo3 5460 fmptco 5478 fnressn 5497 fconst4m 5531 riota2df 5642 eloprabga 5749 frecabcl 6178 mptelixpg 6505 exmidfodomrlemreseldju 6887 enq0breq 7056 genpassl 7144 genpassu 7145 elnnnn0 8777 peano2z 8847 znnsub 8862 znn0sub 8876 uzin 9112 nn01to3 9163 rpnegap 9227 divelunit 9480 elfz5 9493 uzsplit 9567 elfzonelfzo 9702 adddivflid 9760 divfl0 9764 2shfti 10326 rexuz3 10484 clim2c 10733 fisumss 10845 infssuzex 11284 bezoutlemmain 11326 eltg3 11818 mulc1cncf 11918 |
Copyright terms: Public domain | W3C validator |