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

Theorem truan 1548
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 1541 . . 3
21biantrur 530 . 2 (𝜑 ↔ (⊤ ∧ 𝜑))
32bicomi 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