Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > biantru | Structured version Visualization version GIF version |
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-1993.) |
Ref | Expression |
---|---|
biantru.1 | ⊢ 𝜑 |
Ref | Expression |
---|---|
biantru | ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biantru.1 | . 2 ⊢ 𝜑 | |
2 | iba 530 | . 2 ⊢ (𝜑 → (𝜓 ↔ (𝜓 ∧ 𝜑))) | |
3 | 1, 2 | ax-mp 5 | 1 ⊢ (𝜓 ↔ (𝜓 ∧ 𝜑)) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 208 ∧ wa 398 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 209 df-an 399 |
This theorem is referenced by: biantrur 533 pm4.71 560 eu6lem 2654 eu6 2655 isset 3507 rexcom4b 3525 eueq 3699 ssrabeq 4059 nsspssun 4234 disjpss 4410 reusngf 4606 reuprg0 4632 reuprg 4633 pr1eqbg 4781 disjprgw 5054 disjprg 5055 ax6vsep 5200 pwun 5453 dfid3 5457 elvv 5621 elvvv 5622 dfres3 5853 resopab 5897 xpcan2 6029 funfn 6380 dffn2 6511 dffn3 6520 dffn4 6591 fsn 6892 sucexb 7518 fparlem1 7801 fsplitOLD 7807 wfrlem8 7956 ixp0x 8484 ac6sfi 8756 fiint 8789 rankc1 9293 cf0 9667 ccatrcan 14075 prmreclem2 16247 subislly 22083 ovoliunlem1 24097 plyun0 24781 tgjustf 26253 ercgrg 26297 0wlk 27889 0trl 27895 0pth 27898 0cycl 27907 nmoolb 28542 hlimreui 29010 nmoplb 29678 nmfnlb 29695 dmdbr5ati 30193 disjunsn 30338 fsumcvg4 31188 ind1a 31273 issibf 31586 bnj1174 32270 derang0 32411 subfacp1lem6 32427 satfdm 32611 dmscut 33267 bj-denotes 34183 bj-rexcom4bv 34193 bj-rexcom4b 34194 bj-tagex 34294 bj-restuni 34382 rdgeqoa 34645 ftc1anclem5 34965 eqvrelcoss3 35847 dfeldisj5 35948 dibord 38289 ifpnot 39828 ifpdfxor 39846 ifpid1g 39853 ifpim1g 39860 ifpimimb 39863 relopabVD 41228 euabsneu 43256 |
Copyright terms: Public domain | W3C validator |