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  611  imordc  902  drsb1  1845  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  cbvabw  2352  raleqf  2724  rspceaimv  2915  alexeq  2929  mo2icl  2982  sbc19.21g  3097  csbcow  3135  csbiebg  3167  ralss  3290  ifmdc  3645  ssuni  3910  intmin4  3951  ssexg  4223  pocl  4394  frforeq1  4434  frforeq2  4436  frind  4443  ontr2exmid  4617  elirr  4633  en2lp  4646  tfisi  4679  vtoclr  4767  sosng  4792  fun11  5388  funimass4  5684  dff13  5892  f1mpt  5895  isopolem  5946  oprabid  6033  caovcan  6170  caoftrn  6251  dfsmo2  6433  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlembfn  6490  tfr1onlemres  6495  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllembfn  6503  tfrcllemres  6508  tfrcl  6510  qliftfun  6764  ecoptocl  6769  ecopovtrn  6779  ecopovtrng  6782  dom2lem  6923  ssfiexmid  7038  domfiexmid  7040  findcard  7050  findcard2  7051  findcard2s  7052  fiintim  7093  supmoti  7160  eqsupti  7163  suplubti  7167  supisoex  7176  isomnimap  7304  ismkvmap  7321  iswomnimap  7333  tapeq1  7438  ltsonq  7585  prarloclem3  7684  suplocexpr  7912  lttrsr  7949  mulextsr1  7968  suplocsrlem  7995  axpre-lttrn  8071  axpre-mulext  8075  axcaucvglemres  8086  axpre-suploclemres  8088  axpre-suploc  8089  prime  9546  raluz  9773  indstr  9788  supinfneg  9790  infsupneg  9791  fz1sbc  10292  zsupcllemstep  10449  zsupcllemex  10450  zsupssdc  10458  exbtwnzlemshrink  10468  rebtwn2zlemshrink  10473  apexp1  10940  zfz1iso  11063  wrdind  11254  wrd2ind  11255  caucvgre  11492  maxleast  11724  rexanre  11731  rexico  11732  minmax  11741  xrminmax  11776  addcn2  11821  mulcn2  11823  cn1lem  11825  bezoutlemmain  12519  dfgcd2  12535  exprmfct  12660  prmdvdsexpr  12672  sqrt2irr  12684  pw2dvdslemn  12687  prmpwdvds  12878  infpn2  13027  isrrg  14227  istopg  14673  lmbr  14887  metcnp  15186  addcncntoplem  15235  mpodvdsmulf1o  15664  lgseisenlem2  15750  2sqlem6  15799  2sqlem8  15802  2sqlem10  15804  bj-rspgt  16150  bdssexg  16267  strcollnft  16347  sscoll2  16351  nnnninfex  16388