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 299 | . 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-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: mpbirand 439 3anibar 1160 drex1 1791 elrab3t 2885 bnd2 4159 opbrop 4690 opelresi 4902 funcnv3 5260 fnssresb 5310 dff1o5 5451 fneqeql2 5605 fnniniseg2 5619 rexsupp 5620 dffo3 5643 fmptco 5662 fnressn 5682 fconst4m 5716 riota2df 5829 eloprabga 5940 frecabcl 6378 mptelixpg 6712 exmidfodomrlemreseldju 7177 enq0breq 7398 genpassl 7486 genpassu 7487 elnnnn0 9178 peano2z 9248 znnsub 9263 znn0sub 9277 uzin 9519 nn01to3 9576 rpnegap 9643 negelrp 9644 xsubge0 9838 divelunit 9959 elfz5 9973 uzsplit 10048 elfzonelfzo 10186 adddivflid 10248 divfl0 10252 2shfti 10795 rexuz3 10954 clim2c 11247 fisumss 11355 infssuzex 11904 bezoutlemmain 11953 pc2dvds 12283 1arith 12319 eltg3 12851 lmbrf 13009 cnrest2 13030 cnptoprest 13033 cnptoprest2 13034 ismet2 13148 elbl2ps 13186 elbl2 13187 xblpnfps 13192 xblpnf 13193 bdxmet 13295 metcn 13308 cnbl0 13328 cnblcld 13329 mulc1cncf 13370 ellimc3apf 13423 pilem1 13494 lgsdilem 13722 lgsne0 13733 lgsabs1 13734 |
Copyright terms: Public domain | W3C validator |