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  2868  rexcom4b  2885  eueq  3013  nsspssun  3478  disjpss  3581  disjprg  4100  ax9vsep  4226  pwun  4384  dfid3  4392  reusv5OLD  4626  reusv6OLD  4627  reusv7OLD  4628  sucexb  4682  elvv  4830  elvvv  4831  resopab  5078  xpcan2  5195  funfn  5365  dffn2  5473  dffn3  5479  dffn4  5540  fsn  5779  fparlem1  6305  fsplit  6310  ixp0x  6932  ac6sfi  7191  fiint  7223  rankc1  7632  cf0  7967  ccatrcan  11561  prmreclem2  13061  eltopspOLD  16762  subislly  17313  ovoliunlem1  18965  plyun0  19683  nmoolb  21463  hlimreui  21933  nmoplb  22601  nmfnlb  22618  dmdbr5ati  23116  ind1a  23684  derang0  24104  subfacp1lem6  24120  dfres3  24674  wfrlem8  24821  ssrabeq  27403  0wlk  27697  0trl  27698  0pth  27712  relopabVD  28439  bnj1174  28795  dibord  31418
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