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

Theorem imbi2i 215
Description: Introduce an antecedent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 6-Feb-2013.)
Hypothesis
Ref Expression
bi.a (φψ)
Assertion
Ref Expression
imbi2i ((χφ) ↔ (χψ))

Proof of Theorem imbi2i
StepHypRef Expression
1 bi.a . . 3 (φψ)
21a1i 9 . 2 (χ → (φψ))
32pm5.74i 169 1 ((χφ) ↔ (χψ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  imbi12i  228  anidmdbi  378  nan  610  sbcof2  1664  sblimv  1747  sbhb  1789  sblim  1804  2sb6  1833  sbcom2v  1834  2sb6rf  1839  eu1  1898  moabs  1922  mo3h  1926  moanim  1947  2moswapdc  1963  r2alf  2310  r19.21t  2363  reu2  2697  reu8  2705  2reuswapdc  2711  2rmorex  2713  ssconb  3044  ssin  3127  reldisj  3239  ssundifim  3274  ralm  3293  unissb  3573  repizf2lem  3877  elirr  4196  en2lp  4204  tfi  4220  ssrel  4343  ssrel2  4345  fncnv  4879  fun11  4880
  Copyright terms: Public domain W3C validator