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  2312  raleqf  2682  rspceaimv  2864  alexeq  2878  mo2icl  2931  sbc19.21g  3046  csbcow  3083  csbiebg  3114  ralss  3236  ifmdc  3589  ssuni  3846  intmin4  3887  ssexg  4157  pocl  4321  frforeq1  4361  frforeq2  4363  frind  4370  ontr2exmid  4542  elirr  4558  en2lp  4571  tfisi  4604  vtoclr  4692  sosng  4717  fun11  5302  funimass4  5587  dff13  5790  f1mpt  5793  isopolem  5844  oprabid  5928  caovcan  6061  caoftrn  6132  dfsmo2  6312  tfr1onlemsucfn  6365  tfr1onlemsucaccv  6366  tfr1onlembxssdm  6368  tfr1onlembfn  6369  tfr1onlemres  6374  tfrcllemsucfn  6378  tfrcllemsucaccv  6379  tfrcllembxssdm  6381  tfrcllembfn  6382  tfrcllemres  6387  tfrcl  6389  qliftfun  6643  ecoptocl  6648  ecopovtrn  6658  ecopovtrng  6661  dom2lem  6798  ssfiexmid  6904  domfiexmid  6906  findcard  6916  findcard2  6917  findcard2s  6918  fiintim  6957  supmoti  7022  eqsupti  7025  suplubti  7029  supisoex  7038  isomnimap  7165  ismkvmap  7182  iswomnimap  7194  tapeq1  7281  ltsonq  7427  prarloclem3  7526  suplocexpr  7754  lttrsr  7791  mulextsr1  7810  suplocsrlem  7837  axpre-lttrn  7913  axpre-mulext  7917  axcaucvglemres  7928  axpre-suploclemres  7930  axpre-suploc  7931  prime  9382  raluz  9608  indstr  9623  supinfneg  9625  infsupneg  9626  fz1sbc  10126  exbtwnzlemshrink  10279  rebtwn2zlemshrink  10284  apexp1  10730  zfz1iso  10853  caucvgre  11022  maxleast  11254  rexanre  11261  rexico  11262  minmax  11270  xrminmax  11305  addcn2  11350  mulcn2  11352  cn1lem  11354  zsupcllemstep  11978  zsupcllemex  11979  zsupssdc  11987  bezoutlemmain  12031  dfgcd2  12047  exprmfct  12170  prmdvdsexpr  12182  sqrt2irr  12194  pw2dvdslemn  12197  prmpwdvds  12387  infpn2  12507  istopg  13959  lmbr  14173  metcnp  14472  addcncntoplem  14511  lgseisenlem2  14912  2sqlem6  14928  2sqlem8  14931  2sqlem10  14933  bj-rspgt  14999  bdssexg  15117  strcollnft  15197  sscoll2  15201