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  898  drsb1  1810  ax11v2  1831  ax11v  1838  ax11ev  1839  equs5or  1841  cbvabw  2316  raleqf  2686  rspceaimv  2872  alexeq  2886  mo2icl  2939  sbc19.21g  3054  csbcow  3091  csbiebg  3123  ralss  3245  ifmdc  3597  ssuni  3857  intmin4  3898  ssexg  4168  pocl  4334  frforeq1  4374  frforeq2  4376  frind  4383  ontr2exmid  4557  elirr  4573  en2lp  4586  tfisi  4619  vtoclr  4707  sosng  4732  fun11  5321  funimass4  5607  dff13  5811  f1mpt  5814  isopolem  5865  oprabid  5950  caovcan  6083  caoftrn  6158  dfsmo2  6340  tfr1onlemsucfn  6393  tfr1onlemsucaccv  6394  tfr1onlembxssdm  6396  tfr1onlembfn  6397  tfr1onlemres  6402  tfrcllemsucfn  6406  tfrcllemsucaccv  6407  tfrcllembxssdm  6409  tfrcllembfn  6410  tfrcllemres  6415  tfrcl  6417  qliftfun  6671  ecoptocl  6676  ecopovtrn  6686  ecopovtrng  6689  dom2lem  6826  ssfiexmid  6932  domfiexmid  6934  findcard  6944  findcard2  6945  findcard2s  6946  fiintim  6985  supmoti  7052  eqsupti  7055  suplubti  7059  supisoex  7068  isomnimap  7196  ismkvmap  7213  iswomnimap  7225  tapeq1  7312  ltsonq  7458  prarloclem3  7557  suplocexpr  7785  lttrsr  7822  mulextsr1  7841  suplocsrlem  7868  axpre-lttrn  7944  axpre-mulext  7948  axcaucvglemres  7959  axpre-suploclemres  7961  axpre-suploc  7962  prime  9416  raluz  9643  indstr  9658  supinfneg  9660  infsupneg  9661  fz1sbc  10162  exbtwnzlemshrink  10317  rebtwn2zlemshrink  10322  apexp1  10789  zfz1iso  10912  caucvgre  11125  maxleast  11357  rexanre  11364  rexico  11365  minmax  11373  xrminmax  11408  addcn2  11453  mulcn2  11455  cn1lem  11457  zsupcllemstep  12082  zsupcllemex  12083  zsupssdc  12091  bezoutlemmain  12135  dfgcd2  12151  exprmfct  12276  prmdvdsexpr  12288  sqrt2irr  12300  pw2dvdslemn  12303  prmpwdvds  12493  infpn2  12613  isrrg  13759  istopg  14167  lmbr  14381  metcnp  14680  addcncntoplem  14719  lgseisenlem2  15187  2sqlem6  15207  2sqlem8  15210  2sqlem10  15212  bj-rspgt  15278  bdssexg  15396  strcollnft  15476  sscoll2  15480