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

Theorem biantrur 299
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 297 . 2  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
31, 2ax-mp 5 1  |-  ( ps  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 103    <-> wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpbiran  907  truan  1331  rexv  2676  reuv  2677  rmov  2678  rabab  2679  euxfrdc  2841  euind  2842  dfdif3  3154  ddifstab  3176  vss  3378  mptv  3993  regexmidlem1  4416  peano5  4480  intirr  4893  fvopab6  5483  riotav  5701  mpov  5827  brtpos0  6115  frec0g  6260  inl11  6916  apreim  8328  clim0  11005  gcd0id  11574  isbasis3g  12119  opnssneib  12231  ssidcn  12285  bj-d0clsepcl  12957
  Copyright terms: Public domain W3C validator