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  833  truan  1243  rexv  2545  reuv  2546  rmov  2547  rabab  2548  euxfrdc  2700  euind  2701  nssinpss  3142  nsspssun  3143  vss  3237  difsnpssim  3477  mptv  3823  regexmidlem1  4198  peano5  4244  intirr  4634  fvopab6  5185  riotav  5393  mpt2v  5513  brtpos0  5785  frec0g  5898  bj-d0clsepcl  7287
  Copyright terms: Public domain W3C validator