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

Theorem biantru 505
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 26-May-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 503 . 2  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ( ps  /\  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    /\ wa 369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 185  df-an 371
This theorem is referenced by:  pm4.71  630  mpbiran2  912  isset  3112  rexcom4b  3130  eueq  3270  ssrabeq  3581  nsspssun  3726  disjpss  3872  disjprg  4438  ax6vsep  4567  reusv5OLD  4652  reusv6OLD  4653  reusv7OLD  4654  pwun  4783  dfid3  4791  elvv  5052  elvvv  5053  resopab  5313  xpcan2  5437  funfn  5610  dffn2  5725  dffn3  5731  dffn4  5794  fsn  6052  sucexb  6617  fparlem1  6875  fsplit  6880  ixp0x  7489  ac6sfi  7755  fiint  7788  rankc1  8279  cf0  8622  ccatrcan  12650  prmreclem2  14285  eltopspOLD  19181  subislly  19743  ovoliunlem1  21643  plyun0  22324  ercgrg  23631  0wlk  24211  0trl  24212  0pth  24236  nmoolb  25350  hlimreui  25821  nmoplb  26490  nmfnlb  26507  dmdbr5ati  27005  disjunsn  27114  fsumcvg4  27556  ind1a  27662  issibf  27903  derang0  28241  subfacp1lem6  28257  dfres3  28753  wfrlem8  28915  ftc1anclem5  29660  funressnfv  31637  pr1eqbg  31721  relopabVD  32658  bnj1174  33015  bj-denotes  33392  bj-rexcom4bv  33405  bj-rexcom4b  33406  bj-tagex  33503  dibord  35833
  Copyright terms: Public domain W3C validator