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

Theorem biantrur 303
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 301 . 2 (𝜑 → (𝜓 ↔ (𝜑𝜓)))
31, 2ax-mp 5 1 (𝜓 ↔ (𝜑𝜓))
Colors of variables: wff set class
Syntax hints:  wa 104  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  mpbiran  940  truan  1370  rexv  2757  reuv  2758  rmov  2759  rabab  2760  euxfrdc  2925  euind  2926  dfdif3  3247  ddifstab  3269  vss  3472  mptv  4102  regexmidlem1  4534  peano5  4599  intirr  5017  fvopab6  5614  riotav  5838  mpov  5967  brtpos0  6255  frec0g  6400  inl11  7066  apreim  8562  clim0  11295  gcd0id  11982  nnwosdc  12042  isbasis3g  13631  opnssneib  13741  ssidcn  13795  bj-d0clsepcl  14762
  Copyright terms: Public domain W3C validator