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

Theorem trcrm 25054
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  25101  albineal  25102  eel0TT  28784  eelT00  28785  eelTTT  28786  eelT11  28788  eelT12  28792  eelTT1  28794  eelT01  28795  eel0T1  28796  eelTT  28860  uunT1p1  28870  uunTT1  28882  uunTT1p1  28883  uunTT1p2  28884  uunT11  28885  uunT11p1  28886  uunT11p2  28887  uunT12  28888  uunT12p1  28889  uunT12p2  28890  uunT12p3  28891  uunT12p4  28892  uunT12p5  28893
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