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

Theorem biantrurd 293
 Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 1-May-1995.) (Proof shortened by Andrew Salmon, 7-May-2011.)
Hypothesis
Ref Expression
biantrud.1 (𝜑𝜓)
Assertion
Ref Expression
biantrurd (𝜑 → (𝜒 ↔ (𝜓𝜒)))

Proof of Theorem biantrurd
StepHypRef Expression
1 biantrud.1 . 2 (𝜑𝜓)
2 ibar 289 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 14 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ 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:  3anibar  1083  drex1  1695  elrab3t  2720  bnd2  3954  opbrop  4447  opelresi  4651  funcnv3  4989  fnssresb  5039  dff1o5  5163  fneqeql2  5304  fnniniseg2  5318  rexsupp  5319  dffo3  5342  fmptco  5358  fnressn  5377  fconst4m  5409  riota2df  5516  eloprabga  5619  enq0breq  6592  genpassl  6680  genpassu  6681  elnnnn0  8282  peano2z  8338  znnsub  8353  znn0sub  8367  uzin  8601  nn01to3  8649  rpnegap  8713  divelunit  8971  elfz5  8984  uzsplit  9056  elfzonelfzo  9188  adddivflid  9242  divfl0  9246  2shfti  9660  rexuz3  9817  clim2c  10036
 Copyright terms: Public domain W3C validator