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

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

Proof of Theorem biantru
StepHypRef Expression
1 biantru.1 . 2  |-  ph
2 iba 490 . 2  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
31, 2ax-mp 8 1  |-  ( ps  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 177    /\ wa 359
This theorem is referenced by:  pm4.71  612  mpbiran2  886  isset  2960  rexcom4b  2977  eueq  3106  ssrabeq  3429  nsspssun  3574  disjpss  3678  disjprg  4208  ax9vsep  4334  pwun  4491  dfid3  4499  reusv5OLD  4733  reusv6OLD  4734  reusv7OLD  4735  sucexb  4789  elvv  4936  elvvv  4937  resopab  5187  xpcan2  5306  funfn  5482  dffn2  5592  dffn3  5598  dffn4  5659  fsn  5906  fparlem1  6446  fsplit  6451  ixp0x  7090  ac6sfi  7351  fiint  7383  rankc1  7796  cf0  8131  ccatrcan  11779  prmreclem2  13285  eltopspOLD  16983  subislly  17544  ovoliunlem1  19398  plyun0  20116  0wlk  21545  0trl  21546  0pth  21570  nmoolb  22272  hlimreui  22742  nmoplb  23410  nmfnlb  23427  dmdbr5ati  23925  ind1a  24418  issibf  24648  derang0  24855  subfacp1lem6  24871  dfres3  25382  wfrlem8  25545  ftc1anclem5  26284  funressnfv  27968  pr1eqbg  28056  relopabVD  29013  bnj1174  29372  dibord  31957
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