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

Theorem biantrud 300
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 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-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  mpbiran2d  436  posng  4571  elrnmpt1  4750  fliftf  5654  elxp7  6022  eroveu  6474  sbthlemi5  6801  sbthlemi6  6802  elfi2  6812  reapltxor  8269  divap0b  8356  nnle1eq1  8654  nn0le0eq0  8909  nn0lt10b  9035  ioopos  9626  xrmaxiflemcom  10910  fz1f1o  11036  nndivdvds  11347  dvdsmultr2  11381  discld  12148  cncnpi  12239  cnptoprest2  12251  lmss  12257  txcn  12286  isxmet2d  12337  xblss2  12394  bdxmet  12490  xmetxp  12496  cncffvrn  12555
  Copyright terms: Public domain W3C validator