MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biantru 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  2920  rexcom4b  2937  eueq  3066  ssrabeq  3389  nsspssun  3534  disjpss  3638  disjprg  4168  ax9vsep  4294  pwun  4451  dfid3  4459  reusv5OLD  4692  reusv6OLD  4693  reusv7OLD  4694  sucexb  4748  elvv  4895  elvvv  4896  resopab  5146  xpcan2  5265  funfn  5441  dffn2  5551  dffn3  5557  dffn4  5618  fsn  5865  fparlem1  6405  fsplit  6410  ixp0x  7049  ac6sfi  7310  fiint  7342  rankc1  7752  cf0  8087  ccatrcan  11734  prmreclem2  13240  eltopspOLD  16938  subislly  17497  ovoliunlem1  19351  plyun0  20069  0wlk  21498  0trl  21499  0pth  21523  nmoolb  22225  hlimreui  22695  nmoplb  23363  nmfnlb  23380  dmdbr5ati  23878  ind1a  24371  issibf  24601  derang0  24808  subfacp1lem6  24824  dfres3  25330  wfrlem8  25477  funressnfv  27859  pr1eqbg  27944  relopabVD  28722  bnj1174  29078  dibord  31642
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