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

Theorem imbi1i 227
Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 17-Sep-2013.)
Hypothesis
Ref Expression
imbi1i.1
Assertion
Ref Expression
imbi1i

Proof of Theorem imbi1i
StepHypRef Expression
1 imbi1i.1 . 2
2 imbi1 225 . 2
31, 2ax-mp 7 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  ancomsimp  1326  sbrim  1827  sbal1yz  1874  sbmo  1956  mo4f  1957  moanim  1971  necon4addc  2269  necon1bddc  2276  nfraldya  2352  r3al  2360  r19.23t  2417  ceqsralt  2575  ralab  2695  ralrab  2696  euind  2722  reu2  2723  rmo4  2728  reuind  2738  rmo3  2843  raldifb  3077  unss  3111  ralunb  3118  inssdif0im  3285  ssundifim  3300  raaan  3321  pwss  3366  ralsns  3399  disjsn  3423  snss  3485  unissb  3601  intun  3637  intpr  3638  dfiin2g  3681  dftr2  3847  repizf2lem  3905  axpweq  3915  zfpow  3919  axpow2  3920  zfun  4137  uniex2  4139  setindel  4221  setind  4222  elirr  4224  en2lp  4232  tfi  4248  raliunxp  4420  dffun2  4855  dffun4  4856  dffun4f  4861  dffun7  4871  funcnveq  4905  fununi  4910  addnq0mo  6430  mulnq0mo  6431  addsrmo  6671  mulsrmo  6672  prime  8113  raluz2  8298  ralrp  8379  bdcriota  9338  bj-uniex2  9371  bj-ssom  9395
  Copyright terms: Public domain W3C validator