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

Theorem biantrurd 299
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 295 . 2  |-  ( ps 
->  ( ch  <->  ( ps  /\ 
ch ) ) )
31, 2syl 14 1  |-  ( ph  ->  ( ch  <->  ( ps  /\ 
ch ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102    <-> wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  3anibar  1107  drex1  1720  elrab3t  2749  bnd2  3955  opbrop  4445  opelresi  4651  funcnv3  4992  fnssresb  5042  dff1o5  5166  fneqeql2  5308  fnniniseg2  5322  rexsupp  5323  dffo3  5346  fmptco  5362  fnressn  5381  fconst4m  5413  riota2df  5519  eloprabga  5622  frecabcl  6048  enq0breq  6688  genpassl  6776  genpassu  6777  elnnnn0  8398  peano2z  8468  znnsub  8483  znn0sub  8497  uzin  8732  nn01to3  8783  rpnegap  8847  divelunit  9100  elfz5  9113  uzsplit  9185  elfzonelfzo  9316  adddivflid  9374  divfl0  9378  2shfti  9857  rexuz3  10014  clim2c  10261  infssuzex  10489  bezoutlemmain  10531
  Copyright terms: Public domain W3C validator