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

Theorem truan 1454
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  |-  ( ( T.  /\  ph )  <->  ph )

Proof of Theorem truan
StepHypRef Expression
1 tru 1441 . . 3  |- T.
21biantrur 508 . 2  |-  ( ph  <->  ( T.  /\  ph )
)
32bicomi 205 1  |-  ( ( T.  /\  ph )  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370   T. wtru 1438
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 188  df-an 372  df-tru 1440
This theorem is referenced by:  truanfal  1460  euelss  3760  tgcgr4  24574  aciunf1  28267  sgn3da  29420  truconj  32301  tradd  32306  ifpdfbi  36087  ifpdfxor  36101  dfid7  36189  eel0TT  37056  eelT00  37057  eelTTT  37058  eelT11  37060  eelT12  37064  eelTT1  37066  eelT01  37067  eel0T1  37068  eelTT  37131  uunT1p1  37141  uunTT1  37153  uunTT1p1  37154  uunTT1p2  37155  uunT11  37156  uunT11p1  37157  uunT11p2  37158  uunT12  37159  uunT12p1  37160  uunT12p2  37161  uunT12p3  37162  uunT12p4  37163  uunT12p5  37164
  Copyright terms: Public domain W3C validator