ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1i Structured version   GIF 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  1305  sbrim  1808  sbal1yz  1855  sbmo  1937  mo4f  1938  moanim  1952  necon4addc  2249  necon1bddc  2256  nfraldya  2332  r3al  2340  r19.23t  2397  ceqsralt  2554  ralab  2674  ralrab  2675  euind  2701  reu2  2702  rmo4  2707  reuind  2717  rmo3  2822  raldifb  3056  unss  3090  ralunb  3097  inssdif0im  3264  ssundifim  3279  raaan  3302  pwss  3345  ralsns  3378  disjsn  3402  snss  3464  unissb  3580  intun  3616  intpr  3617  dfiin2g  3660  dftr2  3826  repizf2lem  3884  axpweq  3894  zfpow  3898  axpow2  3899  zfun  4117  uniex2  4119  setindel  4201  setind  4202  elirr  4204  en2lp  4212  tfi  4228  raliunxp  4400  dffun2  4835  dffun4  4836  dffun4f  4840  dffun7  4850  funcnveq  4884  fununi  4889  addnq0mo  6296  mulnq0mo  6297  addsrmo  6484  mulsrmo  6485  bdcriota  7249  bj-uniex2  7278  bj-ssom  7297
  Copyright terms: Public domain W3C validator