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

Theorem imbi1d 230
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 157 . . 3  |-  ( ph  ->  ( ch  ->  ps ) )
32imim1d 75 . 2  |-  ( ph  ->  ( ( ps  ->  th )  ->  ( ch  ->  th ) ) )
41biimpd 143 . . 3  |-  ( ph  ->  ( ps  ->  ch ) )
54imim1d 75 . 2  |-  ( ph  ->  ( ( ch  ->  th )  ->  ( ps  ->  th ) ) )
63, 5impbid 128 1  |-  ( ph  ->  ( ( ps  ->  th )  <->  ( ch  ->  th ) ) )
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:  imbi12d  233  imbi1  235  imim21b  251  pm5.33  581  imordc  865  drsb1  1753  ax11v2  1774  ax11v  1781  ax11ev  1782  equs5or  1784  raleqf  2597  rspceaimv  2769  alexeq  2783  mo2icl  2834  sbc19.21g  2947  csbiebg  3010  ralss  3131  ifmdc  3477  ssuni  3726  intmin4  3767  ssexg  4035  pocl  4193  frforeq1  4233  frforeq2  4235  frind  4242  ontr2exmid  4408  elirr  4424  en2lp  4437  tfisi  4469  vtoclr  4555  sosng  4580  fun11  5158  funimass4  5438  dff13  5635  f1mpt  5638  isopolem  5689  oprabid  5769  caovcan  5901  caoftrn  5973  dfsmo2  6150  tfr1onlemsucfn  6203  tfr1onlemsucaccv  6204  tfr1onlembxssdm  6206  tfr1onlembfn  6207  tfr1onlemres  6212  tfrcllemsucfn  6216  tfrcllemsucaccv  6217  tfrcllembxssdm  6219  tfrcllembfn  6220  tfrcllemres  6225  tfrcl  6227  qliftfun  6477  ecoptocl  6482  ecopovtrn  6492  ecopovtrng  6495  dom2lem  6632  ssfiexmid  6736  domfiexmid  6738  findcard  6748  findcard2  6749  findcard2s  6750  fiintim  6783  supmoti  6846  eqsupti  6849  suplubti  6853  supisoex  6862  isomnimap  6975  ismkvmap  6994  ltsonq  7170  prarloclem3  7269  suplocexpr  7497  lttrsr  7534  mulextsr1  7553  suplocsrlem  7580  axpre-lttrn  7656  axpre-mulext  7660  axcaucvglemres  7671  axpre-suploclemres  7673  axpre-suploc  7674  prime  9101  raluz  9322  indstr  9337  supinfneg  9339  infsupneg  9340  fz1sbc  9816  exbtwnzlemshrink  9966  rebtwn2zlemshrink  9971  zfz1iso  10524  caucvgre  10693  maxleast  10925  rexanre  10932  rexico  10933  minmax  10941  xrminmax  10974  addcn2  11019  mulcn2  11021  cn1lem  11023  zsupcllemstep  11534  zsupcllemex  11535  bezoutlemmain  11582  dfgcd2  11598  exprmfct  11714  prmdvdsexpr  11724  sqrt2irr  11736  pw2dvdslemn  11738  istopg  12061  lmbr  12277  metcnp  12576  addcncntoplem  12615  bj-rspgt  12804  bdssexg  12913
  Copyright terms: Public domain W3C validator