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  613  imordc  904  drsb1  1847  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  cbvabw  2354  raleqf  2726  rspceaimv  2918  alexeq  2932  mo2icl  2985  sbc19.21g  3100  csbcow  3138  csbiebg  3170  ralss  3293  ifmdc  3648  ssuni  3915  intmin4  3956  ssexg  4228  pocl  4400  frforeq1  4440  frforeq2  4442  frind  4449  ontr2exmid  4623  elirr  4639  en2lp  4652  tfisi  4685  vtoclr  4774  sosng  4799  fun11  5397  funimass4  5696  dff13  5909  f1mpt  5912  isopolem  5963  oprabid  6050  caovcan  6187  caoftrn  6268  dfsmo2  6453  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemres  6528  tfrcl  6530  qliftfun  6786  ecoptocl  6791  ecopovtrn  6801  ecopovtrng  6804  dom2lem  6945  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  findcard  7077  findcard2  7078  findcard2s  7079  fiintim  7123  supmoti  7192  eqsupti  7195  suplubti  7199  supisoex  7208  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  tapeq1  7471  ltsonq  7618  prarloclem3  7717  suplocexpr  7945  lttrsr  7982  mulextsr1  8001  suplocsrlem  8028  axpre-lttrn  8104  axpre-mulext  8108  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  prime  9579  raluz  9812  indstr  9827  supinfneg  9829  infsupneg  9830  fz1sbc  10331  zsupcllemstep  10490  zsupcllemex  10491  zsupssdc  10499  exbtwnzlemshrink  10509  rebtwn2zlemshrink  10514  apexp1  10981  zfz1iso  11106  wrdind  11307  wrd2ind  11308  caucvgre  11559  maxleast  11791  rexanre  11798  rexico  11799  minmax  11808  xrminmax  11843  addcn2  11888  mulcn2  11890  cn1lem  11892  bezoutlemmain  12587  dfgcd2  12603  exprmfct  12728  prmdvdsexpr  12740  sqrt2irr  12752  pw2dvdslemn  12755  prmpwdvds  12946  infpn2  13095  isrrg  14296  istopg  14742  lmbr  14956  metcnp  15255  addcncntoplem  15304  mpodvdsmulf1o  15733  lgseisenlem2  15819  2sqlem6  15868  2sqlem8  15871  2sqlem10  15873  bj-rspgt  16433  bdssexg  16550  strcollnft  16630  sscoll2  16634  nnnninfex  16675