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

Theorem biantrur 493
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
Hypothesis
Ref Expression
biantrur.1  |-  ph
Assertion
Ref Expression
biantrur  |-  ( ps  <->  (
ph  /\  ps )
)

Proof of Theorem biantrur
StepHypRef Expression
1 biantrur.1 . 2  |-  ph
2 ibar 491 . 2  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
31, 2ax-mp 8 1  |-  ( ps  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  mpbiran  885  rexv  2914  reuv  2915  rmov  2916  rabab  2917  euxfr  3064  euind  3065  ddif  3423  nssinpss  3517  nsspssun  3518  vss  3608  elimif  3712  difsnpss  3885  sspr  3906  sstp  3907  disjprg  4150  mptv  4243  oteqex2  4390  reusv2lem5  4669  reusv7OLD  4676  intirr  5193  xpcan  5246  fvopab6  5766  fnressn  5858  fnsuppres  5892  mpt2v  6103  fparlem2  6387  brtpos0  6423  sorpss  6464  riotav  6491  genpass  8820  nnwos  10477  hashbclem  11629  ccatlcan  11706  clim0  12228  gcd0id  12951  pjfval2  16860  isbasis3g  16938  opnssneib  17103  ssidcn  17242  qtopcld  17667  vieta1  20097  lgsne0  20985  0wlk  21410  0trl  21411  shlesb1i  22737  chnlei  22836  pjneli  23074  cvexchlem  23720  dmdbr5ati  23774  elimifd  23849  elim2if  23850  lmxrge0  24142  cntnevol  24377  dfid4  24963  elpotr  25162  nofulllem1  25381  dfbigcup2  25464  axpasch  25595  isdomn3  27193  bnj110  28568  lub0N  29305  glb0N  29309  cvlsupr3  29460
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 178  df-an 361
  Copyright terms: Public domain W3C validator