Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > truan | Structured version Visualization version GIF version |
Description: True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.) |
Ref | Expression |
---|---|
truan | ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tru 1487 | . . 3 ⊢ ⊤ | |
2 | 1 | biantrur 527 | . 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑)) |
3 | 2 | bicomi 214 | 1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 196 ∧ wa 384 ⊤wtru 1484 |
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 197 df-an 386 df-tru 1486 |
This theorem is referenced by: truanfal 1507 euelss 3914 tgcgr4 25426 aciunf1 29463 sgn3da 30603 truconj 33903 tradd 33907 ifpdfbi 37818 ifpdfxor 37832 dfid7 37919 eel0TT 38929 eelT00 38930 eelTTT 38931 eelT11 38932 eelT12 38934 eelTT1 38935 eelT01 38936 eel0T1 38937 eelTT 38998 uunT1p1 39008 uunTT1 39020 uunTT1p1 39021 uunTT1p2 39022 uunT11 39023 uunT11p1 39024 uunT11p2 39025 uunT12 39026 uunT12p1 39027 uunT12p2 39028 uunT12p3 39029 uunT12p4 39030 uunT12p5 39031 |
Copyright terms: Public domain | W3C validator |