ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  biantrur 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  847  truan  1260  rexv  2572  reuv  2573  rmov  2574  rabab  2575  euxfrdc  2727  euind  2728  nssinpss  3169  nsspssun  3170  vss  3264  difsnpssim  3507  mptv  3853  regexmidlem1  4258  peano5  4321  intirr  4711  fvopab6  5264  riotav  5473  mpt2v  5594  brtpos0  5867  frec0g  5983  apreim  7594  clim0  9806  bj-d0clsepcl  10049
  Copyright terms: Public domain W3C validator