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

Theorem truan 1387
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 1374 . . 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 1371
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 1373
This theorem is referenced by:  truanfal  1395  sgn3da  27060  truconj  29044  tradd  29050  eel0TT  31730  eelT00  31731  eelTTT  31732  eelT11  31734  eelT12  31738  eelTT1  31740  eelT01  31741  eel0T1  31742  eelTT  31806  uunT1p1  31816  uunTT1  31828  uunTT1p1  31829  uunTT1p2  31830  uunT11  31831  uunT11p1  31832  uunT11p2  31833  uunT12  31834  uunT12p1  31835  uunT12p2  31836  uunT12p3  31837  uunT12p4  31838  uunT12p5  31839
  Copyright terms: Public domain W3C validator