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  2952  rexcom4b  2969  eueq  3098  ssrabeq  3421  nsspssun  3566  disjpss  3670  disjprg  4200  ax9vsep  4326  pwun  4483  dfid3  4491  reusv5OLD  4725  reusv6OLD  4726  reusv7OLD  4727  sucexb  4781  elvv  4928  elvvv  4929  resopab  5179  xpcan2  5298  funfn  5474  dffn2  5584  dffn3  5590  dffn4  5651  fsn  5898  fparlem1  6438  fsplit  6443  ixp0x  7082  ac6sfi  7343  fiint  7375  rankc1  7788  cf0  8123  ccatrcan  11771  prmreclem2  13277  eltopspOLD  16975  subislly  17536  ovoliunlem1  19390  plyun0  20108  0wlk  21537  0trl  21538  0pth  21562  nmoolb  22264  hlimreui  22734  nmoplb  23402  nmfnlb  23419  dmdbr5ati  23917  ind1a  24410  issibf  24640  derang0  24847  subfacp1lem6  24863  dfres3  25374  wfrlem8  25537  ftc1anclem5  26274  funressnfv  27959  pr1eqbg  28046  relopabVD  28950  bnj1174  29309  dibord  31894
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