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

Theorem biantru 507
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 505 . 2  |-  ( ph  ->  ( ps  <->  ( ps  /\ 
ph ) ) )
31, 2ax-mp 5 1  |-  ( ps  <->  ( ps  /\  ph )
)
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    /\ wa 370
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 188  df-an 372
This theorem is referenced by:  pm4.71  634  mpbiran2  927  isset  3085  rexcom4b  3103  eueq  3243  ssrabeq  3547  nsspssun  3706  disjpss  3843  disjprg  4416  ax6vsep  4547  pwun  4757  dfid3  4765  elvv  4908  elvvv  4909  resopab  5166  xpcan2  5289  funfn  5626  dffn2  5743  dffn3  5749  dffn4  5812  fsn  6072  sucexb  6646  fparlem1  6903  fsplit  6908  wfrlem8  7047  ixp0x  7554  ac6sfi  7817  fiint  7850  rankc1  8342  cf0  8681  ccatrcan  12819  prmreclem2  14848  subislly  20482  ovoliunlem1  22441  plyun0  23137  ercgrg  24548  0wlk  25260  0trl  25261  0pth  25285  nmoolb  26397  hlimreui  26877  nmoplb  27545  nmfnlb  27562  dmdbr5ati  28060  rabtru  28121  disjunsn  28193  fsumcvg4  28751  ind1a  28837  issibf  29161  bnj1174  29807  derang0  29887  subfacp1lem6  29903  dfres3  30393  bj-denotes  31424  bj-rexcom4bv  31437  bj-rexcom4b  31438  bj-tagex  31536  ftc1anclem5  31934  dibord  34645  ifpnot  36032  ifpdfxor  36050  ifpid1g  36057  ifpim1g  36064  ifpimimb  36067  relopabVD  37158  funressnfv  38341  pr1eqbg  38695
  Copyright terms: Public domain W3C validator