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

Theorem imbi1i 236
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 234 . 2 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
31, 2ax-mp 7 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  imbi12i  237  ancomsimp  1370  sbrim  1873  sbal1yz  1920  sbmo  2002  mo4f  2003  moanim  2017  necon4addc  2319  necon1bddc  2326  nfraldya  2406  r3al  2414  r19.23t  2473  ceqsralt  2637  ralab  2763  ralrab  2764  euind  2790  reu2  2791  rmo4  2796  reuind  2806  rmo3  2916  dfdif3  3094  raldifb  3124  unss  3158  ralunb  3165  inssdif0im  3332  ssundifim  3347  raaan  3369  pwss  3421  ralsnsg  3454  ralsns  3455  disjsn  3478  snss  3540  unissb  3657  intun  3693  intpr  3694  dfiin2g  3737  dftr2  3903  repizf2lem  3961  axpweq  3971  zfpow  3975  axpow2  3976  zfun  4225  uniex2  4227  setindel  4317  setind  4318  elirr  4320  en2lp  4333  zfregfr  4352  tfi  4360  raliunxp  4535  dffun2  4979  dffun4  4980  dffun4f  4985  dffun7  4995  funcnveq  5030  fununi  5035  addnq0mo  6909  mulnq0mo  6910  addsrmo  7192  mulsrmo  7193  prime  8741  raluz2  8962  ralrp  9050  isprm4  10881  bdcriota  11117  bj-uniex2  11150  bj-ssom  11174
  Copyright terms: Public domain W3C validator