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

Theorem imbi1d 229
Description: Deduction adding 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
imbid.1  |-  ( ph  ->  ( ps  <->  ch )
)
Assertion
Ref Expression
imbi1d  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )

Proof of Theorem imbi1d
StepHypRef Expression
1 imbid.1 . . . 4  |-  ( ph  ->  ( ps  <->  ch )
)
21biimprd 156 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 74 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 142 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 74 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 127 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
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:  imbi12d  232  imbi1  234  imim21b  250  pm5.33  574  imordc  830  drsb1  1721  ax11v2  1742  ax11v  1749  ax11ev  1750  equs5or  1752  raleqf  2546  alexeq  2722  mo2icl  2772  sbc19.21g  2883  csbiebg  2946  ralss  3061  ssuni  3631  intmin4  3672  ssexg  3925  pocl  4066  frforeq1  4106  frforeq2  4108  frind  4115  ontr2exmid  4276  elirr  4292  en2lp  4305  tfisi  4336  vtoclr  4414  sosng  4439  fun11  4997  funimass4  5256  dff13  5439  f1mpt  5442  isopolem  5492  oprabid  5568  caovcan  5696  caoftrn  5767  dfsmo2  5936  tfr1onlemsucfn  5989  tfr1onlemsucaccv  5990  tfr1onlembxssdm  5992  tfr1onlembfn  5993  tfr1onlemres  5998  tfrcllemsucfn  6002  tfrcllemsucaccv  6003  tfrcllembxssdm  6005  tfrcllembfn  6006  tfrcllemres  6011  tfrcl  6013  qliftfun  6254  ecoptocl  6259  ecopovtrn  6269  ecopovtrng  6272  dom2lem  6319  ssfiexmid  6411  domfiexmid  6413  findcard  6422  findcard2  6423  findcard2s  6424  supmoti  6465  eqsupti  6468  suplubti  6472  supisoex  6481  ltsonq  6650  prarloclem3  6749  lttrsr  7001  mulextsr1  7019  axpre-lttrn  7112  axpre-mulext  7116  axcaucvglemres  7127  prime  8527  raluz  8747  indstr  8762  supinfneg  8764  infsupneg  8765  fz1sbc  9189  exbtwnzlemshrink  9335  rebtwn2zlemshrink  9340  caucvgre  10005  maxleast  10237  rexanre  10244  rexico  10245  minmax  10250  addcn2  10287  mulcn2  10289  cn1lem  10290  zsupcllemstep  10485  zsupcllemex  10486  bezoutlemmain  10531  dfgcd2  10547  exprmfct  10663  prmdvdsexpr  10673  sqrt2irr  10685  pw2dvdslemn  10687  bj-rspgt  10747  bdssexg  10853
  Copyright terms: Public domain W3C validator