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  439  posng  4615  elrnmpt1  4794  fliftf  5704  elxp7  6072  eroveu  6524  sbthlemi5  6853  sbthlemi6  6854  elfi2  6864  reapltxor  8371  divap0b  8463  nnle1eq1  8764  nn0le0eq0  9025  nn0lt10b  9151  ioopos  9759  xrmaxiflemcom  11046  fz1f1o  11172  nndivdvds  11526  dvdsmultr2  11560  discld  12335  cncnpi  12427  cnptoprest2  12439  lmss  12445  txcn  12474  isxmet2d  12547  xblss2  12604  bdxmet  12700  xmetxp  12706  cncffvrn  12768
 Copyright terms: Public domain W3C validator