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  2815  reuv  2816  rmov  2817  rabab  2818  euxfr  2964  euind  2965  ddif  3321  nssinpss  3414  nsspssun  3415  vss  3504  elimif  3607  difsnpss  3774  sspr  3793  sstp  3794  disjprg  4035  mptv  4128  oteqex2  4274  reusv2lem5  4555  reusv7OLD  4562  intirr  5077  xpcan  5128  fvopab6  5637  fnressn  5721  fnsuppres  5748  mpt2v  5953  fparlem2  6235  brtpos0  6257  sorpss  6298  riotav  6325  genpass  8649  nnwos  10302  hashbclem  11406  ccatlcan  11480  clim0  11996  gcd0id  12718  pjfval2  16625  isbasis3g  16703  opnssneib  16868  ssidcn  17001  qtopcld  17420  vieta1  19708  lgsne0  20588  shlesb1i  21981  chnlei  22080  pjneli  22318  cvexchlem  22964  dmdbr5ati  23018  elimifd  23167  elim2if  23168  cntnevol  23191  lmxrge0  23390  elpotr  24208  nofulllem1  24427  dfbigcup2  24510  axpasch  24641  sallnei  25632  isdomn3  27626  0wlk  28343  0trl  28344  bnj110  29206  lub0N  30001  glb0N  30005  cvlsupr3  30156
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