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

Theorem truan 1518
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 1511 . . 3
21biantrur 523 . 2 (𝜑 ↔ (⊤ ∧ 𝜑))
32bicomi 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