![]() |
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 301 | . 2 ⊢ (𝜓 → (𝜒 ↔ (𝜓 ∧ 𝜒))) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (𝜒 ↔ (𝜓 ∧ 𝜒))) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ 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: mpbirand 441 3anibar 1165 drex1 1798 elrab3t 2894 bnd2 4175 opbrop 4707 opelresi 4920 funcnv3 5280 fnssresb 5330 dff1o5 5472 fneqeql2 5628 fnniniseg2 5642 rexsupp 5643 dffo3 5666 fmptco 5685 fnressn 5705 fconst4m 5739 riota2df 5854 eloprabga 5965 frecabcl 6403 mptelixpg 6737 exmidfodomrlemreseldju 7202 enq0breq 7438 genpassl 7526 genpassu 7527 elnnnn0 9222 peano2z 9292 znnsub 9307 znn0sub 9321 uzin 9563 nn01to3 9620 rpnegap 9689 negelrp 9690 xsubge0 9884 divelunit 10005 elfz5 10020 uzsplit 10095 elfzonelfzo 10233 adddivflid 10295 divfl0 10299 2shfti 10843 rexuz3 11002 clim2c 11295 fisumss 11403 infssuzex 11953 bezoutlemmain 12002 pc2dvds 12332 1arith 12368 xpsfrnel 12770 xpsfrnel2 12772 lsslss 13506 eltg3 13745 lmbrf 13903 cnrest2 13924 cnptoprest 13927 cnptoprest2 13928 ismet2 14042 elbl2ps 14080 elbl2 14081 xblpnfps 14086 xblpnf 14087 bdxmet 14189 metcn 14202 cnbl0 14222 cnblcld 14223 mulc1cncf 14264 ellimc3apf 14317 pilem1 14388 lgsdilem 14616 lgsne0 14627 lgsabs1 14628 |
Copyright terms: Public domain | W3C validator |