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

Theorem truan 1614
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 1600 . . 3
21biantrur 528 . 2 (𝜑 ↔ (⊤ ∧ 𝜑))
32bicomi 214 1 ((⊤ ∧ 𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 383  wtru 1597
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 385  df-tru 1599
This theorem is referenced by:  truanfal  1620  euelss  4022  tgcgr4  25546  aciunf1  29693  sgn3da  30833  truconj  34135  tradd  34139  ifpdfbi  38237  ifpdfxor  38251  dfid7  38338  eel0TT  39348  eelT00  39349  eelTTT  39350  eelT11  39351  eelT12  39353  eelTT1  39354  eelT01  39355  eel0T1  39356  eelTT  39417  uunT1p1  39427  uunTT1  39439  uunTT1p1  39440  uunTT1p2  39441  uunT11  39442  uunT11p1  39443  uunT11p2  39444  uunT12  39445  uunT12p1  39446  uunT12p2  39447  uunT12p3  39448  uunT12p4  39449  uunT12p5  39450
  Copyright terms: Public domain W3C validator