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  625  sbcof2  1688  sblimv  1771  sbhb  1813  sblim  1828  2sb6  1857  sbcom2v  1858  2sb6rf  1863  eu1  1922  moabs  1946  mo3h  1950  moanim  1971  2moswapdc  1987  r2alf  2335  r19.21t  2388  reu2  2723  reu8  2731  2reuswapdc  2737  2rmorex  2739  ssconb  3070  ssin  3153  reldisj  3265  ssundifim  3300  ralm  3319  unissb  3601  repizf2lem  3905  elirr  4224  en2lp  4232  tfi  4248  ssrel  4371  ssrel2  4373  fncnv  4908  fun11  4909  raluz2  8298
  Copyright terms: Public domain W3C validator