ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biantrurd Structured version   Unicode version

Theorem biantrurd 289
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypothesis
Ref Expression
biantrud.1
Assertion
Ref Expression
biantrurd

Proof of Theorem biantrurd
StepHypRef Expression
1 biantrud.1 . 2
2 ibar 285 . 2
31, 2syl 14 1
Colors of variables: wff set class
Syntax hints:   wi 4   wa 97   wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3anibar  1071  drex1  1676  elrab3t  2691  bnd2  3917  opbrop  4362  opelresi  4566  funcnv3  4904  fnssresb  4954  dff1o5  5078  fneqeql2  5219  fnniniseg2  5233  rexsupp  5234  dffo3  5257  fmptco  5273  fnressn  5292  fconst4m  5324  riota2df  5431  eloprabga  5533  enq0breq  6418  genpassl  6507  genpassu  6508  elnnnn0  7961  peano2z  8017  znnsub  8032  znn0sub  8045  uzin  8241  nn01to3  8288  rpnegap  8350  divelunit  8600  elfz5  8612  uzsplit  8684  elfzonelfzo  8816
  Copyright terms: Public domain W3C validator