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

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

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  604  imordc  892  drsb1  1792  ax11v2  1813  ax11v  1820  ax11ev  1821  equs5or  1823  cbvabw  2293  raleqf  2661  rspceaimv  2842  alexeq  2856  mo2icl  2909  sbc19.21g  3023  csbcow  3060  csbiebg  3091  ralss  3213  ifmdc  3565  ssuni  3818  intmin4  3859  ssexg  4128  pocl  4288  frforeq1  4328  frforeq2  4330  frind  4337  ontr2exmid  4509  elirr  4525  en2lp  4538  tfisi  4571  vtoclr  4659  sosng  4684  fun11  5265  funimass4  5547  dff13  5747  f1mpt  5750  isopolem  5801  oprabid  5885  caovcan  6017  caoftrn  6086  dfsmo2  6266  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlembfn  6323  tfr1onlemres  6328  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllembfn  6336  tfrcllemres  6341  tfrcl  6343  qliftfun  6595  ecoptocl  6600  ecopovtrn  6610  ecopovtrng  6613  dom2lem  6750  ssfiexmid  6854  domfiexmid  6856  findcard  6866  findcard2  6867  findcard2s  6868  fiintim  6906  supmoti  6970  eqsupti  6973  suplubti  6977  supisoex  6986  isomnimap  7113  ismkvmap  7130  iswomnimap  7142  ltsonq  7360  prarloclem3  7459  suplocexpr  7687  lttrsr  7724  mulextsr1  7743  suplocsrlem  7770  axpre-lttrn  7846  axpre-mulext  7850  axcaucvglemres  7861  axpre-suploclemres  7863  axpre-suploc  7864  prime  9311  raluz  9537  indstr  9552  supinfneg  9554  infsupneg  9555  fz1sbc  10052  exbtwnzlemshrink  10205  rebtwn2zlemshrink  10210  apexp1  10652  zfz1iso  10776  caucvgre  10945  maxleast  11177  rexanre  11184  rexico  11185  minmax  11193  xrminmax  11228  addcn2  11273  mulcn2  11275  cn1lem  11277  zsupcllemstep  11900  zsupcllemex  11901  zsupssdc  11909  bezoutlemmain  11953  dfgcd2  11969  exprmfct  12092  prmdvdsexpr  12104  sqrt2irr  12116  pw2dvdslemn  12119  prmpwdvds  12307  infpn2  12411  istopg  12791  lmbr  13007  metcnp  13306  addcncntoplem  13345  2sqlem6  13750  2sqlem8  13753  2sqlem10  13755  bj-rspgt  13821  bdssexg  13939  strcollnft  14019  sscoll2  14023