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  2805  rexcom4b  2822  eueq  2950  nsspssun  3415  disjpss  3518  disjprg  4035  ax9vsep  4161  pwun  4318  dfid3  4326  reusv5OLD  4560  reusv6OLD  4561  reusv7OLD  4562  sucexb  4616  elvv  4764  elvvv  4765  resopab  5012  xpcan2  5129  funfn  5299  dffn2  5406  dffn3  5412  dffn4  5473  fsn  5712  fparlem1  6234  fsplit  6239  ixp0x  6860  ac6sfi  7117  fiint  7149  rankc1  7558  cf0  7893  ccatrcan  11481  prmreclem2  12980  eltopspOLD  16672  subislly  17223  ovoliunlem1  18877  plyun0  19595  nmoolb  21365  hlimreui  21835  nmoplb  22503  nmfnlb  22520  dmdbr5ati  23018  ind1a  23619  derang0  23715  subfacp1lem6  23731  dfres3  24187  wfrlem8  24334  0wlk  28343  0trl  28344  0pth  28356  relopabVD  28993  bnj1174  29349  dibord  31971
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