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

Theorem imbi2i 225
 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 179 1 ((𝜒𝜑) ↔ (𝜒𝜓))
 Colors of variables: wff set class Syntax hints:   → wi 4   ↔ 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:  imbi12i  238  anidmdbi  393  nan  664  sbcof2  1764  sblimv  1848  sbhb  1891  sblim  1906  2sb6  1935  sbcom2v  1936  2sb6rf  1941  eu1  2000  moabs  2024  mo3h  2028  moanim  2049  2moswapdc  2065  r2alf  2426  r19.21t  2481  rspc2gv  2771  reu2  2841  reu8  2849  2reuswapdc  2857  2rmorex  2859  dfdif3  3152  ssconb  3175  ssin  3264  reldisj  3380  ssundifim  3412  ralm  3433  unissb  3732  repizf2lem  4045  elirr  4416  en2lp  4429  tfi  4456  ssrel  4587  ssrel2  4589  fncnv  5147  fun11  5148  axcaucvglemres  7634  suprzclex  9053  raluz2  9276  supinfneg  9292  infsupneg  9293  infssuzex  11490  bezoutlemmain  11532  isprm2  11644  lmres  12259  limcdifap  12587
 Copyright terms: Public domain W3C validator