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  2873  alexeq  2887  mo2icl  2940  sbc19.21g  3055  csbcow  3092  csbiebg  3124  ralss  3246  ifmdc  3598  ssuni  3858  intmin4  3899  ssexg  4169  pocl  4335  frforeq1  4375  frforeq2  4377  frind  4384  ontr2exmid  4558  elirr  4574  en2lp  4587  tfisi  4620  vtoclr  4708  sosng  4733  fun11  5322  funimass4  5608  dff13  5812  f1mpt  5815  isopolem  5866  oprabid  5951  caovcan  6085  caoftrn  6160  dfsmo2  6342  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlembfn  6399  tfr1onlemres  6404  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllembfn  6412  tfrcllemres  6417  tfrcl  6419  qliftfun  6673  ecoptocl  6678  ecopovtrn  6688  ecopovtrng  6691  dom2lem  6828  ssfiexmid  6934  domfiexmid  6936  findcard  6946  findcard2  6947  findcard2s  6948  fiintim  6987  supmoti  7054  eqsupti  7057  suplubti  7061  supisoex  7070  isomnimap  7198  ismkvmap  7215  iswomnimap  7227  tapeq1  7314  ltsonq  7460  prarloclem3  7559  suplocexpr  7787  lttrsr  7824  mulextsr1  7843  suplocsrlem  7870  axpre-lttrn  7946  axpre-mulext  7950  axcaucvglemres  7961  axpre-suploclemres  7963  axpre-suploc  7964  prime  9419  raluz  9646  indstr  9661  supinfneg  9663  infsupneg  9664  fz1sbc  10165  exbtwnzlemshrink  10320  rebtwn2zlemshrink  10325  apexp1  10792  zfz1iso  10915  caucvgre  11128  maxleast  11360  rexanre  11367  rexico  11368  minmax  11376  xrminmax  11411  addcn2  11456  mulcn2  11458  cn1lem  11460  zsupcllemstep  12085  zsupcllemex  12086  zsupssdc  12094  bezoutlemmain  12138  dfgcd2  12154  exprmfct  12279  prmdvdsexpr  12291  sqrt2irr  12303  pw2dvdslemn  12306  prmpwdvds  12496  infpn2  12616  isrrg  13762  istopg  14178  lmbr  14392  metcnp  14691  addcncntoplem  14740  lgseisenlem2  15228  2sqlem6  15277  2sqlem8  15280  2sqlem10  15282  bj-rspgt  15348  bdssexg  15466  strcollnft  15546  sscoll2  15550