![]() |
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 1541 | . . 3 ⊢ ⊤ | |
2 | 1 | biantrur 530 | . 2 ⊢ (𝜑 ↔ (⊤ ∧ 𝜑)) |
3 | 2 | bicomi 224 | 1 ⊢ ((⊤ ∧ 𝜑) ↔ 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: ↔ wb 206 ∧ wa 395 ⊤wtru 1538 |
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 207 df-an 396 df-tru 1540 |
This theorem is referenced by: truanfal 1571 euelss 4346 tgcgr4 28548 aciunf1 32673 sgn3da 34498 wl-2mintru1 37404 truconj 38009 tradd 38013 ifpdfxor 43389 dfid7 43514 eel0TT 44615 eelT00 44616 eelTTT 44617 eelT11 44618 eelT12 44620 eelTT1 44621 eelT01 44622 eel0T1 44623 eelTT 44682 uunT1p1 44692 uunTT1 44704 uunTT1p1 44705 uunTT1p2 44706 uunT11 44707 uunT11p1 44708 uunT11p2 44709 uunT12 44710 uunT12p1 44711 uunT12p2 44712 uunT12p3 44713 uunT12p4 44714 uunT12p5 44715 |
Copyright terms: Public domain | W3C validator |