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  4346  tgcgr4  28548  aciunf1  32673  sgn3da  34498  wl-2mintru1  37404  truconj  38009  tradd  38013  ifpdfxor  43389  dfid7  43514  eel0TT  44615  eelT00  44616  eelTTT  44617  eelT11  44618  eelT12  44620  eelTT1  44621  eelT01  44622  eel0T1  44623  eelTT  44682  uunT1p1  44692  uunTT1  44704  uunTT1p1  44705  uunTT1p2  44706  uunT11  44707  uunT11p1  44708  uunT11p2  44709  uunT12  44710  uunT12p1  44711  uunT12p2  44712  uunT12p3  44713  uunT12p4  44714  uunT12p5  44715
  Copyright terms: Public domain W3C validator