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

Theorem biantrur 297
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 295 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 7 1 (𝜓 ↔ (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mpbiran  886  truan  1306  rexv  2637  reuv  2638  rmov  2639  rabab  2640  euxfrdc  2799  euind  2800  dfdif3  3108  ddifstab  3130  vss  3327  mptv  3927  regexmidlem1  4339  peano5  4403  intirr  4805  fvopab6  5380  riotav  5595  mpt2v  5720  brtpos0  5999  frec0g  6144  apreim  8056  clim0  10637  gcd0id  11052  bj-d0clsepcl  11466
  Copyright terms: Public domain W3C validator