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

Theorem biantrur 301
 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 299 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜑𝜓))
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 106  ax-ia3 107 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  mpbiran  925  truan  1352  rexv  2730  reuv  2731  rmov  2732  rabab  2733  euxfrdc  2898  euind  2899  dfdif3  3217  ddifstab  3239  vss  3441  mptv  4061  regexmidlem1  4490  peano5  4555  intirr  4969  fvopab6  5561  riotav  5779  mpov  5905  brtpos0  6193  frec0g  6338  inl11  6999  apreim  8461  clim0  11164  gcd0id  11843  isbasis3g  12404  opnssneib  12516  ssidcn  12570  bj-d0clsepcl  13459
 Copyright terms: Public domain W3C validator