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

Theorem imbi1i 237
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 235 . 2 ((𝜑𝜓) → ((𝜑𝜒) ↔ (𝜓𝜒)))
31, 2ax-mp 5 1 ((𝜑𝜒) ↔ (𝜓𝜒))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 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  ancomsimp  1399  sbrim  1905  sbal1yz  1952  sbmo  2034  mo4f  2035  moanim  2049  necon4addc  2353  necon1bddc  2360  nfraldya  2444  r3al  2452  r19.23t  2514  ceqsralt  2685  ralab  2815  ralrab  2816  euind  2842  reu2  2843  rmo4  2848  rmo3f  2852  rmo4f  2853  reuind  2860  rmo3  2970  dfdif3  3154  raldifb  3184  unss  3218  ralunb  3225  inssdif0im  3398  ssundifim  3414  raaan  3437  pwss  3494  ralsnsg  3529  ralsns  3530  disjsn  3553  snss  3617  unissb  3734  intun  3770  intpr  3771  dfiin2g  3814  dftr2  3996  repizf2lem  4053  axpweq  4063  zfpow  4067  axpow2  4068  zfun  4324  uniex2  4326  setindel  4421  setind  4422  elirr  4424  en2lp  4437  zfregfr  4456  tfi  4464  raliunxp  4648  dffun2  5101  dffun4  5102  dffun4f  5107  dffun7  5118  funcnveq  5154  fununi  5159  fiintim  6783  addnq0mo  7219  mulnq0mo  7220  addsrmo  7515  mulsrmo  7516  prime  9101  raluz2  9323  ralrp  9411  modfsummod  11167  isprm4  11696  dedekindicc  12674  bdcriota  12892  bj-uniex2  12925  bj-ssom  12945
  Copyright terms: Public domain W3C validator