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  910  isset  2975  rexcom4b  2993  eueq  3130  ssrabeq  3437  nsspssun  3582  disjpss  3728  disjprg  4287  ax6vsep  4416  reusv5OLD  4501  reusv6OLD  4502  reusv7OLD  4503  pwun  4628  dfid3  4636  elvv  4896  elvvv  4897  resopab  5152  xpcan2  5274  funfn  5446  dffn2  5559  dffn3  5565  dffn4  5625  fsn  5880  sucexb  6419  fparlem1  6671  fsplit  6676  ixp0x  7290  ac6sfi  7555  fiint  7587  rankc1  8076  cf0  8419  ccatrcan  12366  prmreclem2  13977  eltopspOLD  18522  subislly  19084  ovoliunlem1  20984  plyun0  21664  ercgrg  22968  0wlk  23443  0trl  23444  0pth  23468  nmoolb  24170  hlimreui  24641  nmoplb  25310  nmfnlb  25327  dmdbr5ati  25825  disjunsn  25935  fsumcvg4  26379  ind1a  26476  issibf  26718  derang0  27056  subfacp1lem6  27072  dfres3  27568  wfrlem8  27730  ftc1anclem5  28469  funressnfv  30032  pr1eqbg  30119  relopabVD  31635  bnj1174  31992  bj-denotes  32367  bj-rexcom4bv  32380  bj-rexcom4b  32381  bj-tagex  32478  dibord  34802
  Copyright terms: Public domain W3C validator