Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  truan Structured version   Visualization version   GIF version

Theorem truan 1549
 Description: True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.) (Proof shortened by Wolf Lammen, 21-Jul-2019.)
Assertion
Ref Expression
truan ((⊤ ∧ 𝜑) ↔ 𝜑)

Proof of Theorem truan
StepHypRef Expression
1 tru 1542 . . 3
21biantrur 534 . 2 (𝜑 ↔ (⊤ ∧ 𝜑))
32bicomi 227 1 ((⊤ ∧ 𝜑) ↔ 𝜑)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 209   ∧ wa 399  ⊤wtru 1539 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 210  df-an 400  df-tru 1541 This theorem is referenced by:  truanfal  1572  euelss  4264  tgcgr4  26323  aciunf1  30416  sgn3da  31873  wl-2mintru1  34866  truconj  35497  tradd  35501  ifpdfxor  40125  dfid7  40242  eel0TT  41344  eelT00  41345  eelTTT  41346  eelT11  41347  eelT12  41349  eelTT1  41350  eelT01  41351  eel0T1  41352  eelTT  41411  uunT1p1  41421  uunTT1  41433  uunTT1p1  41434  uunTT1p2  41435  uunT11  41436  uunT11p1  41437  uunT11p2  41438  uunT12  41439  uunT12p1  41440  uunT12p2  41441  uunT12p3  41442  uunT12p4  41443  uunT12p5  41444
 Copyright terms: Public domain W3C validator