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  1813  ax11v2  1834  ax11v  1841  ax11ev  1842  equs5or  1844  cbvabw  2319  raleqf  2689  rspceaimv  2876  alexeq  2890  mo2icl  2943  sbc19.21g  3058  csbcow  3095  csbiebg  3127  ralss  3249  ifmdc  3601  ssuni  3861  intmin4  3902  ssexg  4172  pocl  4338  frforeq1  4378  frforeq2  4380  frind  4387  ontr2exmid  4561  elirr  4577  en2lp  4590  tfisi  4623  vtoclr  4711  sosng  4736  fun11  5325  funimass4  5611  dff13  5815  f1mpt  5818  isopolem  5869  oprabid  5954  caovcan  6088  caoftrn  6163  dfsmo2  6345  tfr1onlemsucfn  6398  tfr1onlemsucaccv  6399  tfr1onlembxssdm  6401  tfr1onlembfn  6402  tfr1onlemres  6407  tfrcllemsucfn  6411  tfrcllemsucaccv  6412  tfrcllembxssdm  6414  tfrcllembfn  6415  tfrcllemres  6420  tfrcl  6422  qliftfun  6676  ecoptocl  6681  ecopovtrn  6691  ecopovtrng  6694  dom2lem  6831  ssfiexmid  6937  domfiexmid  6939  findcard  6949  findcard2  6950  findcard2s  6951  fiintim  6992  supmoti  7059  eqsupti  7062  suplubti  7066  supisoex  7075  isomnimap  7203  ismkvmap  7220  iswomnimap  7232  tapeq1  7319  ltsonq  7465  prarloclem3  7564  suplocexpr  7792  lttrsr  7829  mulextsr1  7848  suplocsrlem  7875  axpre-lttrn  7951  axpre-mulext  7955  axcaucvglemres  7966  axpre-suploclemres  7968  axpre-suploc  7969  prime  9425  raluz  9652  indstr  9667  supinfneg  9669  infsupneg  9670  fz1sbc  10171  zsupcllemstep  10319  zsupcllemex  10320  zsupssdc  10328  exbtwnzlemshrink  10338  rebtwn2zlemshrink  10343  apexp1  10810  zfz1iso  10933  caucvgre  11146  maxleast  11378  rexanre  11385  rexico  11386  minmax  11395  xrminmax  11430  addcn2  11475  mulcn2  11477  cn1lem  11479  bezoutlemmain  12165  dfgcd2  12181  exprmfct  12306  prmdvdsexpr  12318  sqrt2irr  12330  pw2dvdslemn  12333  prmpwdvds  12524  infpn2  12673  isrrg  13819  istopg  14235  lmbr  14449  metcnp  14748  addcncntoplem  14797  mpodvdsmulf1o  15226  lgseisenlem2  15312  2sqlem6  15361  2sqlem8  15364  2sqlem10  15366  bj-rspgt  15432  bdssexg  15550  strcollnft  15630  sscoll2  15634