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

Theorem truan 1649
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 1635 . . 3
21biantrur 520 . 2 (𝜑 ↔ (⊤ ∧ 𝜑))
32bicomi 214 1 ((⊤ ∧ 𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 382  wtru 1632
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 383  df-tru 1634
This theorem is referenced by:  truanfal  1655  euelss  4062  tgcgr4  25647  aciunf1  29803  sgn3da  30943  truconj  34235  tradd  34239  ifpdfbi  38344  ifpdfxor  38358  dfid7  38445  eel0TT  39454  eelT00  39455  eelTTT  39456  eelT11  39457  eelT12  39459  eelTT1  39460  eelT01  39461  eel0T1  39462  eelTT  39523  uunT1p1  39533  uunTT1  39545  uunTT1p1  39546  uunTT1p2  39547  uunT11  39548  uunT11p1  39549  uunT11p2  39550  uunT12  39551  uunT12p1  39552  uunT12p2  39553  uunT12p3  39554  uunT12p4  39555  uunT12p5  39556
  Copyright terms: Public domain W3C validator