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

Theorem biantrur 298
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
Hypothesis
Ref Expression
biantrur.1  |-  ph
Assertion
Ref Expression
biantrur  |-  ( ps  <->  (
ph  /\  ps )
)

Proof of Theorem biantrur
StepHypRef Expression
1 biantrur.1 . 2  |-  ph
2 ibar 296 . 2  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
31, 2ax-mp 7 1  |-  ( ps  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpbiran  887  truan  1307  rexv  2638  reuv  2639  rmov  2640  rabab  2641  euxfrdc  2802  euind  2803  dfdif3  3111  ddifstab  3133  vss  3334  mptv  3941  regexmidlem1  4362  peano5  4426  intirr  4831  fvopab6  5410  riotav  5627  mpt2v  5752  brtpos0  6031  frec0g  6176  apreim  8134  clim0  10727  gcd0id  11302  isbasis3g  11798  bj-d0clsepcl  12086
  Copyright terms: Public domain W3C validator