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  919  isset  3113  rexcom4b  3131  eueq  3271  ssrabeq  3582  nsspssun  3738  disjpss  3880  disjprg  4452  ax6vsep  4582  reusv5OLD  4666  reusv6OLD  4667  reusv7OLD  4668  pwun  4797  dfid3  4805  elvv  5067  elvvv  5068  resopab  5330  xpcan2  5451  funfn  5623  dffn2  5738  dffn3  5744  dffn4  5807  fsn  6070  sucexb  6643  fparlem1  6899  fsplit  6904  ixp0x  7516  ac6sfi  7782  fiint  7815  rankc1  8305  cf0  8648  ccatrcan  12710  prmreclem2  14447  eltopspOLD  19546  subislly  20108  ovoliunlem1  22039  plyun0  22720  ercgrg  24034  0wlk  24674  0trl  24675  0pth  24699  nmoolb  25813  hlimreui  26284  nmoplb  26953  nmfnlb  26970  dmdbr5ati  27468  rabtru  27527  disjunsn  27593  fsumcvg4  28093  ind1a  28195  issibf  28472  derang0  28810  subfacp1lem6  28826  dfres3  29406  wfrlem8  29567  ftc1anclem5  30299  funressnfv  32416  pr1eqbg  32561  relopabVD  33844  bnj1174  34202  bj-denotes  34577  bj-rexcom4bv  34590  bj-rexcom4b  34591  bj-tagex  34688  dibord  37029  ifpid1g  37852  ifpim1g  37861  ifpimimb  37862  ifpnot  37864  ifpdfxor  37892
  Copyright terms: Public domain W3C validator