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

Theorem biantru 491
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 489 . 2  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
31, 2ax-mp 8 1  |-  ( ps  <->  ( ps  /\  ph )
)
Colors of variables: wff set class
Syntax hints:    <-> wb 176    /\ wa 358
This theorem is referenced by:  pm4.71  611  mpbiran2  885  isset  2792  rexcom4b  2809  eueq  2937  nsspssun  3402  disjpss  3505  disjprg  4019  ax9vsep  4145  pwun  4302  dfid3  4310  reusv5OLD  4544  reusv6OLD  4545  reusv7OLD  4546  sucexb  4600  elvv  4748  elvvv  4749  resopab  4996  xpcan2  5113  funfn  5283  dffn2  5390  dffn3  5396  dffn4  5457  fsn  5696  fparlem1  6218  fsplit  6223  ixp0x  6844  ac6sfi  7101  fiint  7133  rankc1  7542  cf0  7877  ccatrcan  11465  prmreclem2  12964  eltopspOLD  16656  subislly  17207  ovoliunlem1  18861  plyun0  19579  nmoolb  21349  hlimreui  21819  nmoplb  22487  nmfnlb  22504  dmdbr5ati  23002  ind1a  23604  derang0  23700  subfacp1lem6  23716  dfres3  24116  wfrlem8  24263  relopabVD  28677  bnj1174  29033  dibord  31349
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