Theorem imbi1d 231

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

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4 |- ( ph -> ( ps <-> ch ) )
2	1	biimprd 158	. . 3 |- ( ph -> ( ch -> ps ) )
3	2	imim1d 75	. 2 |- ( ph -> ( ( ps -> th ) -> ( ch -> th ) ) )
4	1	biimpd 144	. . 3 |- ( ph -> ( ps -> ch ) )
5	4	imim1d 75	. 2 |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )
6	3, 5	impbid 129	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )

Syntax hints:   -> wi 4   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  imbi12d  234  imbi1  236  imim21b  253  pm5.33  609  imordc  899  drsb1  1822  ax11v2  1843  ax11v  1850  ax11ev  1851  equs5or  1853  cbvabw  2328  raleqf  2698  rspceaimv  2885  alexeq  2899  mo2icl  2952  sbc19.21g  3067  csbcow  3104  csbiebg  3136  ralss  3259  ifmdc  3612  ssuni  3872  intmin4  3913  ssexg  4183  pocl  4350  frforeq1  4390  frforeq2  4392  frind  4399  ontr2exmid  4573  elirr  4589  en2lp  4602  tfisi  4635  vtoclr  4723  sosng  4748  fun11  5341  funimass4  5629  dff13  5837  f1mpt  5840  isopolem  5891  oprabid  5976  caovcan  6111  caoftrn  6191  dfsmo2  6373  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlembfn  6430  tfr1onlemres  6435  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllembfn  6443  tfrcllemres  6448  tfrcl  6450  qliftfun  6704  ecoptocl  6709  ecopovtrn  6719  ecopovtrng  6722  dom2lem  6863  ssfiexmid  6973  domfiexmid  6975  findcard  6985  findcard2  6986  findcard2s  6987  fiintim  7028  supmoti  7095  eqsupti  7098  suplubti  7102  supisoex  7111  isomnimap  7239  ismkvmap  7256  iswomnimap  7268  tapeq1  7364  ltsonq  7511  prarloclem3  7610  suplocexpr  7838  lttrsr  7875  mulextsr1  7894  suplocsrlem  7921  axpre-lttrn  7997  axpre-mulext  8001  axcaucvglemres  8012  axpre-suploclemres  8014  axpre-suploc  8015  prime  9472  raluz  9699  indstr  9714  supinfneg  9716  infsupneg  9717  fz1sbc  10218  zsupcllemstep  10372  zsupcllemex  10373  zsupssdc  10381  exbtwnzlemshrink  10391  rebtwn2zlemshrink  10396  apexp1  10863  zfz1iso  10986  caucvgre  11292  maxleast  11524  rexanre  11531  rexico  11532  minmax  11541  xrminmax  11576  addcn2  11621  mulcn2  11623  cn1lem  11625  bezoutlemmain  12319  dfgcd2  12335  exprmfct  12460  prmdvdsexpr  12472  sqrt2irr  12484  pw2dvdslemn  12487  prmpwdvds  12678  infpn2  12827  isrrg  14025  istopg  14471  lmbr  14685  metcnp  14984  addcncntoplem  15033  mpodvdsmulf1o  15462  lgseisenlem2  15548  2sqlem6  15597  2sqlem8  15600  2sqlem10  15602  bj-rspgt  15722  bdssexg  15840  strcollnft  15920  sscoll2  15924  nnnninfex  15959