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

Theorem biantrur 291
 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 289 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 7 1 (𝜓 ↔ (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 101   ↔ wb 102 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 104  ax-ia3 105 This theorem depends on definitions:  df-bi 114 This theorem is referenced by:  mpbiran  858  truan  1276  rexv  2589  reuv  2590  rmov  2591  rabab  2592  euxfrdc  2750  euind  2751  nssinpss  3197  nsspssun  3198  vss  3292  difsnpssim  3535  mptv  3881  regexmidlem1  4286  peano5  4349  intirr  4739  fvopab6  5292  riotav  5501  mpt2v  5622  brtpos0  5898  frec0g  6014  apreim  7668  clim0  10037  bj-d0clsepcl  10436
 Copyright terms: Public domain W3C validator