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

Theorem biantrur 297
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 295 . 2  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
31, 2ax-mp 7 1  |-  ( ps  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    /\ 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:  mpbiran  882  truan  1302  rexv  2628  reuv  2629  rmov  2630  rabab  2631  euxfrdc  2789  euind  2790  dfdif3  3094  ddifstab  3116  vss  3312  mptv  3900  regexmidlem1  4312  peano5  4376  intirr  4773  fvopab6  5341  riotav  5552  mpt2v  5673  brtpos0  5949  frec0g  6094  apreim  7980  clim0  10498  gcd0id  10750  bj-d0clsepcl  11163
  Copyright terms: Public domain W3C validator