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

Theorem biantrurd 300
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 296 . 2 (𝜓 → (𝜒 ↔ (𝜓𝜒)))
31, 2syl 14 1 (𝜑 → (𝜒 ↔ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103  wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  3anibar  1112  drex1  1727  elrab3t  2771  bnd2  4014  opbrop  4530  opelresi  4737  funcnv3  5089  fnssresb  5139  dff1o5  5275  fneqeql2  5422  fnniniseg2  5436  rexsupp  5437  dffo3  5460  fmptco  5478  fnressn  5497  fconst4m  5531  riota2df  5642  eloprabga  5749  frecabcl  6178  mptelixpg  6505  exmidfodomrlemreseldju  6887  enq0breq  7056  genpassl  7144  genpassu  7145  elnnnn0  8777  peano2z  8847  znnsub  8862  znn0sub  8876  uzin  9112  nn01to3  9163  rpnegap  9227  divelunit  9480  elfz5  9493  uzsplit  9567  elfzonelfzo  9702  adddivflid  9760  divfl0  9764  2shfti  10326  rexuz3  10484  clim2c  10733  fisumss  10845  infssuzex  11284  bezoutlemmain  11326  eltg3  11818  mulc1cncf  11918
  Copyright terms: Public domain W3C validator