![]() |
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 1511 | . . 3 ⊢ ⊤ | |
2 | 1 | biantrur 523 | . 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑)) |
3 | 2 | bicomi 216 | 1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 198 ∧ wa 387 ⊤wtru 1508 |
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 199 df-an 388 df-tru 1510 |
This theorem is referenced by: truanfal 1541 euelss 4171 tgcgr4 26013 aciunf1 30164 sgn3da 31445 truconj 34823 tradd 34827 ifpdfbi 39235 ifpdfxor 39249 dfid7 39335 eel0TT 40457 eelT00 40458 eelTTT 40459 eelT11 40460 eelT12 40462 eelTT1 40463 eelT01 40464 eel0T1 40465 eelTT 40524 uunT1p1 40534 uunTT1 40546 uunTT1p1 40547 uunTT1p2 40548 uunT11 40549 uunT11p1 40550 uunT11p2 40551 uunT12 40552 uunT12p1 40553 uunT12p2 40554 uunT12p3 40555 uunT12p4 40556 uunT12p5 40557 |
Copyright terms: Public domain | W3C validator |