ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biantrurd 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  |-  ( ph  ->  ps )
Assertion
Ref Expression
biantrurd  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )

Proof of Theorem biantrurd
StepHypRef Expression
1 biantrud.1 . 2  |-  ( ph  ->  ps )
2 ibar 285 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
31, 2syl 14 1  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )
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  1072  drex1  1679  elrab3t  2697  bnd2  3926  opbrop  4419  opelresi  4623  funcnv3  4961  fnssresb  5011  dff1o5  5135  fneqeql2  5276  fnniniseg2  5290  rexsupp  5291  dffo3  5314  fmptco  5330  fnressn  5349  fconst4m  5381  riota2df  5488  eloprabga  5591  enq0breq  6534  genpassl  6622  genpassu  6623  elnnnn0  8225  peano2z  8281  znnsub  8296  znn0sub  8309  uzin  8505  nn01to3  8552  rpnegap  8615  divelunit  8870  elfz5  8882  uzsplit  8954  elfzonelfzo  9086  adddivflid  9134  divfl0  9138  2shfti  9432  rexuz3  9588  clim2c  9805
  Copyright terms: Public domain W3C validator