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

Theorem biantrur 492
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 490 . 2  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
31, 2ax-mp 8 1  |-  ( ps  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  mpbiran  884  rexv  2802  reuv  2803  rmov  2804  rabab  2805  euxfr  2951  euind  2952  ddif  3308  nssinpss  3401  nsspssun  3402  vss  3491  elimif  3594  difsnpss  3758  sspr  3777  sstp  3778  disjprg  4019  mptv  4112  oteqex2  4258  reusv2lem5  4539  reusv7OLD  4546  intirr  5061  xpcan  5112  fvopab6  5621  fnressn  5705  fnsuppres  5732  mpt2v  5937  fparlem2  6219  brtpos0  6241  sorpss  6282  riotav  6309  genpass  8633  nnwos  10286  hashbclem  11390  ccatlcan  11464  clim0  11980  gcd0id  12702  pjfval2  16609  isbasis3g  16687  opnssneib  16852  ssidcn  16985  qtopcld  17404  vieta1  19692  lgsne0  20572  shlesb1i  21965  chnlei  22064  pjneli  22302  cvexchlem  22948  dmdbr5ati  23002  elimifd  23151  elim2if  23152  cntnevol  23175  lmxrge0  23375  elpotr  24137  nofulllem1  24356  dfbigcup2  24439  axpasch  24569  sallnei  25529  isdomn3  27523  bnj110  28890  lub0N  29379  glb0N  29383  cvlsupr3  29534
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
  Copyright terms: Public domain W3C validator