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

Theorem truan 1498
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 1484 . . 3
21biantrur 527 . 2 (𝜑 ↔ (⊤ ∧ 𝜑))
32bicomi 214 1 ((⊤ ∧ 𝜑) ↔ 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wb 196  wa 384  wtru 1481
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 386  df-tru 1483
This theorem is referenced by:  truanfal  1504  euelss  3895  tgcgr4  25339  aciunf1  29323  sgn3da  30402  truconj  33562  tradd  33566  ifpdfbi  37326  ifpdfxor  37340  dfid7  37427  eel0TT  38438  eelT00  38439  eelTTT  38440  eelT11  38441  eelT12  38443  eelTT1  38444  eelT01  38445  eel0T1  38446  eelTT  38507  uunT1p1  38517  uunTT1  38529  uunTT1p1  38530  uunTT1p2  38531  uunT11  38532  uunT11p1  38533  uunT11p2  38534  uunT12  38535  uunT12p1  38536  uunT12p2  38537  uunT12p3  38538  uunT12p4  38539  uunT12p5  38540
  Copyright terms: Public domain W3C validator