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

Proof of Theorem imbi1i
StepHypRef Expression
1 imbi1i.1 . 2  |-  ( ph  <->  ps )
2 imbi1 234 . 2  |-  ( (
ph 
<->  ps )  ->  (
( ph  ->  ch )  <->  ( ps  ->  ch )
) )
31, 2ax-mp 7 1  |-  ( (
ph  ->  ch )  <->  ( ps  ->  ch ) )
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  2405  r3al  2413  r19.23t  2472  ceqsralt  2635  ralab  2761  ralrab  2762  euind  2788  reu2  2789  rmo4  2794  reuind  2804  rmo3  2914  dfdif3  3092  raldifb  3122  unss  3156  ralunb  3163  inssdif0im  3327  ssundifim  3342  raaan  3364  pwss  3415  ralsnsg  3448  ralsns  3449  disjsn  3472  snss  3534  unissb  3651  intun  3687  intpr  3688  dfiin2g  3731  dftr2  3897  repizf2lem  3955  axpweq  3965  zfpow  3969  axpow2  3970  zfun  4217  uniex2  4219  setindel  4309  setind  4310  elirr  4312  en2lp  4325  zfregfr  4344  tfi  4351  raliunxp  4525  dffun2  4962  dffun4  4963  dffun4f  4968  dffun7  4978  funcnveq  5013  fununi  5018  addnq0mo  6751  mulnq0mo  6752  addsrmo  7034  mulsrmo  7035  prime  8579  raluz2  8800  ralrp  8888  isprm4  10708  bdcriota  10941  bj-uniex2  10974  bj-ssom  10998
  Copyright terms: Public domain W3C validator