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

Theorem imbi1i 231
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 229 . 2 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
31, 2ax-mp 7 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114
This theorem is referenced by:  imbi12i  232  ancomsimp  1345  sbrim  1846  sbal1yz  1893  sbmo  1975  mo4f  1976  moanim  1990  necon4addc  2290  necon1bddc  2297  nfraldya  2375  r3al  2383  r19.23t  2440  ceqsralt  2598  ralab  2723  ralrab  2724  euind  2750  reu2  2751  rmo4  2756  reuind  2766  rmo3  2876  raldifb  3110  unss  3144  ralunb  3151  inssdif0im  3318  ssundifim  3333  raaan  3354  pwss  3401  ralsnsg  3434  ralsns  3435  disjsn  3459  snss  3521  unissb  3637  intun  3673  intpr  3674  dfiin2g  3717  dftr2  3883  repizf2lem  3941  axpweq  3951  zfpow  3955  axpow2  3956  zfun  4198  uniex2  4200  setindel  4290  setind  4291  elirr  4293  en2lp  4305  zfregfr  4325  tfi  4332  raliunxp  4504  dffun2  4939  dffun4  4940  dffun4f  4945  dffun7  4955  funcnveq  4989  fununi  4994  addnq0mo  6602  mulnq0mo  6603  addsrmo  6885  mulsrmo  6886  prime  8395  raluz2  8617  ralrp  8701  bdcriota  10369  bj-uniex2  10402  bj-ssom  10426
  Copyright terms: Public domain W3C validator