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  899  drsb1  1822  ax11v2  1843  ax11v  1850  ax11ev  1851  equs5or  1853  cbvabw  2328  raleqf  2698  rspceaimv  2885  alexeq  2899  mo2icl  2952  sbc19.21g  3067  csbcow  3104  csbiebg  3136  ralss  3259  ifmdc  3612  ssuni  3872  intmin4  3913  ssexg  4184  pocl  4351  frforeq1  4391  frforeq2  4393  frind  4400  ontr2exmid  4574  elirr  4590  en2lp  4603  tfisi  4636  vtoclr  4724  sosng  4749  fun11  5342  funimass4  5631  dff13  5839  f1mpt  5842  isopolem  5893  oprabid  5978  caovcan  6113  caoftrn  6193  dfsmo2  6375  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlembfn  6432  tfr1onlemres  6437  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllembfn  6445  tfrcllemres  6450  tfrcl  6452  qliftfun  6706  ecoptocl  6711  ecopovtrn  6721  ecopovtrng  6724  dom2lem  6865  ssfiexmid  6975  domfiexmid  6977  findcard  6987  findcard2  6988  findcard2s  6989  fiintim  7030  supmoti  7097  eqsupti  7100  suplubti  7104  supisoex  7113  isomnimap  7241  ismkvmap  7258  iswomnimap  7270  tapeq1  7366  ltsonq  7513  prarloclem3  7612  suplocexpr  7840  lttrsr  7877  mulextsr1  7896  suplocsrlem  7923  axpre-lttrn  7999  axpre-mulext  8003  axcaucvglemres  8014  axpre-suploclemres  8016  axpre-suploc  8017  prime  9474  raluz  9701  indstr  9716  supinfneg  9718  infsupneg  9719  fz1sbc  10220  zsupcllemstep  10374  zsupcllemex  10375  zsupssdc  10383  exbtwnzlemshrink  10393  rebtwn2zlemshrink  10398  apexp1  10865  zfz1iso  10988  caucvgre  11325  maxleast  11557  rexanre  11564  rexico  11565  minmax  11574  xrminmax  11609  addcn2  11654  mulcn2  11656  cn1lem  11658  bezoutlemmain  12352  dfgcd2  12368  exprmfct  12493  prmdvdsexpr  12505  sqrt2irr  12517  pw2dvdslemn  12520  prmpwdvds  12711  infpn2  12860  isrrg  14058  istopg  14504  lmbr  14718  metcnp  15017  addcncntoplem  15066  mpodvdsmulf1o  15495  lgseisenlem2  15581  2sqlem6  15630  2sqlem8  15633  2sqlem10  15635  bj-rspgt  15759  bdssexg  15877  strcollnft  15957  sscoll2  15961  nnnninfex  15996