ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  imbi1i Unicode 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  |-  ( ph  <->  ps )
Assertion
Ref Expression
imbi1i  |-  ( (
ph  ->  ch )  <->  ( ps  ->  ch ) )

Proof of Theorem imbi1i
StepHypRef Expression
1 imbi1i.1 . 2  |-  ( ph  <->  ps )
2 imbi1 235 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ch )  <->  ( ps  ->  ch )
) )
31, 2ax-mp 5 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  ch ) )
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  1416  sbrim  1929  sbal1yz  1976  sbmo  2058  mo4f  2059  moanim  2073  necon4addc  2378  necon1bddc  2385  nfraldya  2469  r3al  2477  r19.23t  2539  ceqsralt  2713  ralab  2844  ralrab  2845  euind  2871  reu2  2872  rmo4  2877  rmo3f  2881  rmo4f  2882  reuind  2889  rmo3  3000  dfdif3  3186  raldifb  3216  unss  3250  ralunb  3257  inssdif0im  3430  ssundifim  3446  raaan  3469  pwss  3526  ralsnsg  3561  ralsns  3562  disjsn  3585  snss  3649  unissb  3766  intun  3802  intpr  3803  dfiin2g  3846  dftr2  4028  repizf2lem  4085  axpweq  4095  zfpow  4099  axpow2  4100  zfun  4356  uniex2  4358  setindel  4453  setind  4454  elirr  4456  en2lp  4469  zfregfr  4488  tfi  4496  raliunxp  4680  dffun2  5133  dffun4  5134  dffun4f  5139  dffun7  5150  funcnveq  5186  fununi  5191  fiintim  6817  addnq0mo  7262  mulnq0mo  7263  addsrmo  7558  mulsrmo  7559  prime  9157  raluz2  9381  ralrp  9470  modfsummod  11234  isprm4  11807  dedekindicclemicc  12789  bdcriota  13111  bj-uniex2  13144  bj-ssom  13164
  Copyright terms: Public domain W3C validator