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

Theorem truan 1416
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 1403 . . 3  |- T.
21biantrur 504 . 2  |-  ( ph  <->  ( T.  /\  ph )
)
32bicomi 202 1  |-  ( ( T.  /\  ph )  <->  ph )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 367   T. wtru 1400
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 369  df-tru 1402
This theorem is referenced by:  truanfal  1424  euelss  3727  aciunf1  27683  sgn3da  28703  truconj  30707  tradd  30713  eel0TT  33871  eelT00  33872  eelTTT  33873  eelT11  33875  eelT12  33879  eelTT1  33881  eelT01  33882  eel0T1  33883  eelTT  33947  uunT1p1  33957  uunTT1  33969  uunTT1p1  33970  uunTT1p2  33971  uunT11  33972  uunT11p1  33973  uunT11p2  33974  uunT12  33975  uunT12p1  33976  uunT12p2  33977  uunT12p3  33978  uunT12p4  33979  uunT12p5  33980  ifpdfbi  38195  ifpdfxor  38201
  Copyright terms: Public domain W3C validator