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

Theorem biantrud 302
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 298 . 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-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpbiran2d  440  posng  4683  elrnmpt1  4862  fliftf  5778  elxp7  6149  eroveu  6604  sbthlemi5  6938  sbthlemi6  6939  elfi2  6949  reapltxor  8508  divap0b  8600  nnle1eq1  8902  nn0le0eq0  9163  nn0lt10b  9292  ioopos  9907  xrmaxiflemcom  11212  fz1f1o  11338  nndivdvds  11758  dvdsmultr2  11795  pcmpt  12295  pcmpt2  12296  discld  12930  cncnpi  13022  cnptoprest2  13034  lmss  13040  txcn  13069  isxmet2d  13142  xblss2  13199  bdxmet  13295  xmetxp  13301  cncffvrn  13363  lgsneg  13719  lgsdilem  13722
  Copyright terms: Public domain W3C validator