MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biantrur Structured version   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  2962  reuv  2963  rmov  2964  rabab  2965  euxfr  3112  euind  3113  ddif  3471  nssinpss  3565  nsspssun  3566  vss  3656  elimif  3760  difsnpss  3933  sspr  3954  sstp  3955  disjprg  4200  mptv  4293  oteqex2  4440  reusv2lem5  4720  reusv7OLD  4727  intirr  5244  xpcan  5297  fvopab6  5818  fnressn  5910  fnsuppres  5944  mpt2v  6155  fparlem2  6439  brtpos0  6478  sorpss  6519  riotav  6546  genpass  8878  nnwos  10536  hashbclem  11693  ccatlcan  11770  clim0  12292  gcd0id  13015  pjfval2  16928  isbasis3g  17006  opnssneib  17171  ssidcn  17311  qtopcld  17737  vieta1  20221  lgsne0  21109  0wlk  21537  0trl  21538  shlesb1i  22880  chnlei  22979  pjneli  23217  cvexchlem  23863  dmdbr5ati  23917  elimifd  23996  elim2if  23997  lmxrge0  24329  cntnevol  24574  dfid4  25175  elpotr  25400  nofulllem1  25649  dfbigcup2  25736  axpasch  25872  cnambfre  26245  isdomn3  27491  bnj110  29166  lub0N  29924  glb0N  29928  cvlsupr3  30079
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