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

Theorem truan 1396
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 1383 . . 3  |- T.
21biantrur 506 . 2  |-  ( ph  <->  ( T.  /\  ph )
)
32bicomi 202 1  |-  ( ( T.  /\  ph )  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369   T. wtru 1380
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 185  df-an 371  df-tru 1382
This theorem is referenced by:  truanfal  1404  sgn3da  28120  truconj  30104  tradd  30110  eel0TT  32572  eelT00  32573  eelTTT  32574  eelT11  32576  eelT12  32580  eelTT1  32582  eelT01  32583  eel0T1  32584  eelTT  32648  uunT1p1  32658  uunTT1  32670  uunTT1p1  32671  uunTT1p2  32672  uunT11  32673  uunT11p1  32674  uunT11p2  32675  uunT12  32676  uunT12p1  32677  uunT12p2  32678  uunT12p3  32679  uunT12p4  32680  uunT12p5  32681
  Copyright terms: Public domain W3C validator