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

Theorem biantrur 287
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 3-Aug-1994.)
Hypothesis
Ref Expression
biantrur.1 φ
Assertion
Ref Expression
biantrur (ψ ↔ (φ ψ))

Proof of Theorem biantrur
StepHypRef Expression
1 biantrur.1 . 2 φ
2 ibar 285 . 2 (φ → (ψ ↔ (φ ψ)))
31, 2ax-mp 7 1 (ψ ↔ (φ ψ))
Colors of variables: wff set class
Syntax hints:   wa 97  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  mpbiran  846  truan  1259  rexv  2566  reuv  2567  rmov  2568  rabab  2569  euxfrdc  2721  euind  2722  nssinpss  3163  nsspssun  3164  vss  3258  difsnpssim  3498  mptv  3844  regexmidlem1  4218  peano5  4264  intirr  4654  fvopab6  5207  riotav  5416  mpt2v  5536  brtpos0  5808  frec0g  5922  apreim  7367  bj-d0clsepcl  9360
  Copyright terms: Public domain W3C validator