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 ) ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imbi12d  234  imbi1  236  imim21b  253  pm5.33  617  imordc  909  drsb1  1852  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  cbvabw  2363  raleqf  2745  rspceaimv  2938  alexeq  2952  mo2icl  3005  sbc19.21g  3120  csbcow  3158  csbiebg  3190  ralss  3314  ifmdc  3683  ssuni  3957  intmin4  3998  ssexg  4274  pocl  4450  frforeq1  4490  frforeq2  4492  frind  4499  ontr2exmid  4674  elirr  4690  en2lp  4703  tfisi  4736  vtoclr  4825  sosng  4850  fun11  5451  funimass4  5756  dff13  5977  f1mpt  5980  isopolem  6031  oprabid  6120  caovcan  6257  caoftrn  6339  dfsmo2  6562  tfr1onlemsucfn  6615  tfr1onlemsucaccv  6616  tfr1onlembxssdm  6618  tfr1onlembfn  6619  tfr1onlemres  6624  tfrcllemsucfn  6628  tfrcllemsucaccv  6629  tfrcllembxssdm  6631  tfrcllembfn  6632  tfrcllemres  6637  tfrcl  6639  qliftfun  6895  ecoptocl  6900  ecopovtrn  6910  ecopovtrng  6913  dom2lem  7062  ssfiexmid  7182  ssfiexmidt  7184  domfiexmid  7186  findcard  7196  findcard2  7197  findcard2s  7198  fiintim  7242  supmoti  7339  eqsupti  7342  suplubti  7346  supisoex  7355  isomnimap  7483  ismkvmap  7500  iswomnimap  7512  tapeq1  7624  ltsonq  7771  prarloclem3  7870  suplocexpr  8098  lttrsr  8135  mulextsr1  8154  suplocsrlem  8181  axpre-lttrn  8257  axpre-mulext  8261  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  prime  9756  raluz  9994  indstr  10009  supinfneg  10011  infsupneg  10012  fz1sbc  10520  zsupcllemstep  10679  zsupcllemex  10680  zsupssdc  10690  exbtwnzlemshrink  10700  rebtwn2zlemshrink  10705  apexp1  11178  zfz1iso  11315  wrdind  11516  wrd2ind  11517  caucvgre  11769  maxleast  12002  rexanre  12009  rexico  12010  minmax  12020  xrminmax  12056  addcn2  12101  mulcn2  12103  cn1lem  12105  bezoutlemmain  12800  dfgcd2  12816  exprmfct  12942  prmdvdsexpr  12954  sqrt2irr  12966  pwbdvdslemn  12969  prmpwdvds  13163  infpn2  13405  isrrg  14680  opprdrng  14729  istopg  15225  lmbr  15439  metcnp  15738  addcncntoplem  15787  mpodvdsmulf1o  16284  ppiublem1  16291  lgseisenlem2  16395  2sqlem6  16444  2sqlem8  16447  2sqlem10  16449  bj-rspgt  17019  bdssexg  17135  strcollnft  17215  sscoll2  17219  exmidcon  17242  exmidpeirce  17243  nnnninfex  17271