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  1401  sbrim  1907  sbal1yz  1954  sbmo  2036  mo4f  2037  moanim  2051  necon4addc  2355  necon1bddc  2362  nfraldya  2446  r3al  2454  r19.23t  2516  ceqsralt  2687  ralab  2817  ralrab  2818  euind  2844  reu2  2845  rmo4  2850  rmo3f  2854  rmo4f  2855  reuind  2862  rmo3  2972  dfdif3  3156  raldifb  3186  unss  3220  ralunb  3227  inssdif0im  3400  ssundifim  3416  raaan  3439  pwss  3496  ralsnsg  3531  ralsns  3532  disjsn  3555  snss  3619  unissb  3736  intun  3772  intpr  3773  dfiin2g  3816  dftr2  3998  repizf2lem  4055  axpweq  4065  zfpow  4069  axpow2  4070  zfun  4326  uniex2  4328  setindel  4423  setind  4424  elirr  4426  en2lp  4439  zfregfr  4458  tfi  4466  raliunxp  4650  dffun2  5103  dffun4  5104  dffun4f  5109  dffun7  5120  funcnveq  5156  fununi  5161  fiintim  6785  addnq0mo  7223  mulnq0mo  7224  addsrmo  7519  mulsrmo  7520  prime  9118  raluz2  9342  ralrp  9431  modfsummod  11195  isprm4  11727  dedekindicclemicc  12706  bdcriota  13008  bj-uniex2  13041  bj-ssom  13061
  Copyright terms: Public domain W3C validator