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

Theorem biantrud 298
Description: A wff is equivalent to its conjunction with truth. (Contributed by NM, 2-Aug-1994.) (Proof shortened by Wolf Lammen, 23-Oct-2013.)
Hypothesis
Ref Expression
biantrud.1 (𝜑𝜓)
Assertion
Ref Expression
biantrud (𝜑 → (𝜒 ↔ (𝜒𝜓)))

Proof of Theorem biantrud
StepHypRef Expression
1 biantrud.1 . 2 (𝜑𝜓)
2 iba 294 . 2 (𝜓 → (𝜒 ↔ (𝜒𝜓)))
31, 2syl 14 1 (𝜑 → (𝜒 ↔ (𝜒𝜓)))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  posng  4510  elrnmpt1  4686  fliftf  5578  elxp7  5941  eroveu  6381  sbthlemi5  6668  sbthlemi6  6669  reapltxor  8064  divap0b  8148  nnle1eq1  8444  nn0le0eq0  8699  nn0lt10b  8825  ioopos  9366  fz1f1o  10760  nndivdvds  11076  dvdsmultr2  11110  cncffvrn  11593
  Copyright terms: Public domain W3C validator