![]() |
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 4351 tgcgr4 28557 aciunf1 32681 sgn3da 34506 wl-2mintru1 37456 truconj 38061 tradd 38065 ifpdfxor 43449 dfid7 43574 eel0TT 44675 eelT00 44676 eelTTT 44677 eelT11 44678 eelT12 44680 eelTT1 44681 eelT01 44682 eel0T1 44683 eelTT 44742 uunT1p1 44752 uunTT1 44764 uunTT1p1 44765 uunTT1p2 44766 uunT11 44767 uunT11p1 44768 uunT11p2 44769 uunT12 44770 uunT12p1 44771 uunT12p2 44772 uunT12p3 44773 uunT12p4 44774 uunT12p5 44775 |
Copyright terms: Public domain | W3C validator |