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

Theorem biantrur 303
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 301 . 2  |-  ( ph  ->  ( ps  <->  ( ph  /\ 
ps ) ) )
31, 2ax-mp 5 1  |-  ( ps  <->  (
ph  /\  ps )
)
Colors of variables: wff set class
Syntax hints:    /\ wa 104    <-> wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  mpbiran  940  truan  1370  rexv  2755  reuv  2756  rmov  2757  rabab  2758  euxfrdc  2923  euind  2924  dfdif3  3245  ddifstab  3267  vss  3470  mptv  4097  regexmidlem1  4528  peano5  4593  intirr  5010  fvopab6  5607  riotav  5829  mpov  5958  brtpos0  6246  frec0g  6391  inl11  7057  apreim  8537  clim0  11264  gcd0id  11950  nnwosdc  12010  isbasis3g  13177  opnssneib  13289  ssidcn  13343  bj-d0clsepcl  14299
  Copyright terms: Public domain W3C validator