Users' Mathboxes Mathbox for Frédéric Liné < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  trcrm Unicode version

Theorem trcrm 24951
Description: True can be removed from a conjunction. (Contributed by FL, 20-Mar-2011.)
Assertion
Ref Expression
trcrm  |-  ( (  T.  /\  ph )  <->  ph )

Proof of Theorem trcrm
StepHypRef Expression
1 simpr 447 . 2  |-  ( (  T.  /\  ph )  ->  ph )
2 a1tru 1321 . . 3  |-  ( ph  ->  T.  )
32ancri 535 . 2  |-  ( ph  ->  (  T.  /\  ph ) )
41, 3impbii 180 1  |-  ( (  T.  /\  ph )  <->  ph )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358    T. wtru 1307
This theorem is referenced by:  evpexun  24998  albineal  24999  eel0TT  28479  eelT00  28480  eelTTT  28481  eelT11  28483  eelT12  28486  eelTT1  28488  eelT01  28489  eel0T1  28490  eelTT  28546  uunT1p1  28556  uunTT1  28568  uunTT1p1  28569  uunTT1p2  28570  uunT11  28571  uunT11p1  28572  uunT11p2  28573  uunT12  28574  uunT12p1  28575  uunT12p2  28576  uunT12p3  28577  uunT12p4  28578  uunT12p5  28579
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310
  Copyright terms: Public domain W3C validator