MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  biantru 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
Assertion
Ref Expression
biantru

Proof of Theorem biantru
StepHypRef Expression
1 biantru.1 . 2
2 iba 503 . 2
31, 2ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  pm4.71  630  mpbiran2  919  isset  3113  rexcom4b  3131  eueq  3271  ssrabeq  3585  nsspssun  3730  disjpss  3877  disjprg  4448  ax6vsep  4577  reusv5OLD  4662  reusv6OLD  4663  reusv7OLD  4664  pwun  4793  dfid3  4801  elvv  5063  elvvv  5064  resopab  5325  xpcan2  5449  funfn  5622  dffn2  5737  dffn3  5743  dffn4  5806  fsn  6069  sucexb  6644  fparlem1  6900  fsplit  6905  ixp0x  7517  ac6sfi  7784  fiint  7817  rankc1  8309  cf0  8652  ccatrcan  12698  prmreclem2  14435  eltopspOLD  19419  subislly  19982  ovoliunlem1  21913  plyun0  22594  ercgrg  23908  0wlk  24547  0trl  24548  0pth  24572  nmoolb  25686  hlimreui  26157  nmoplb  26826  nmfnlb  26843  dmdbr5ati  27341  disjunsn  27453  fsumcvg4  27932  ind1a  28034  issibf  28275  derang0  28613  subfacp1lem6  28629  dfres3  29188  wfrlem8  29350  ftc1anclem5  30094  funressnfv  32213  pr1eqbg  32297  relopabVD  33701  bnj1174  34059  bj-denotes  34434  bj-rexcom4bv  34447  bj-rexcom4b  34448  bj-tagex  34545  dibord  36886  bj-ifid1g  37708  bj-ifim1g  37714  bj-ifimimb  37715  bj-ifnot  37717  bj-ifdfxor  37732
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
  Copyright terms: Public domain W3C validator