Theorem imbi1d 230

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 157	. . 3 |- ( ph -> ( ch -> ps ) )
3	2	imim1d 75	. 2 |- ( ph -> ( ( ps -> th ) -> ( ch -> th ) ) )
4	1	biimpd 143	. . 3 |- ( ph -> ( ps -> ch ) )
5	4	imim1d 75	. 2 |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )
6	3, 5	impbid 128	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )

Syntax hints:   -> wi 4   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12d  233  imbi1  235  imim21b  251  pm5.33  599  imordc  887  drsb1  1787  ax11v2  1808  ax11v  1815  ax11ev  1816  equs5or  1818  cbvabw  2289  raleqf  2657  rspceaimv  2838  alexeq  2852  mo2icl  2905  sbc19.21g  3019  csbcow  3056  csbiebg  3087  ralss  3208  ifmdc  3558  ssuni  3811  intmin4  3852  ssexg  4121  pocl  4281  frforeq1  4321  frforeq2  4323  frind  4330  ontr2exmid  4502  elirr  4518  en2lp  4531  tfisi  4564  vtoclr  4652  sosng  4677  fun11  5255  funimass4  5537  dff13  5736  f1mpt  5739  isopolem  5790  oprabid  5874  caovcan  6006  caoftrn  6075  dfsmo2  6255  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlembfn  6312  tfr1onlemres  6317  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllembfn  6325  tfrcllemres  6330  tfrcl  6332  qliftfun  6583  ecoptocl  6588  ecopovtrn  6598  ecopovtrng  6601  dom2lem  6738  ssfiexmid  6842  domfiexmid  6844  findcard  6854  findcard2  6855  findcard2s  6856  fiintim  6894  supmoti  6958  eqsupti  6961  suplubti  6965  supisoex  6974  isomnimap  7101  ismkvmap  7118  iswomnimap  7130  ltsonq  7339  prarloclem3  7438  suplocexpr  7666  lttrsr  7703  mulextsr1  7722  suplocsrlem  7749  axpre-lttrn  7825  axpre-mulext  7829  axcaucvglemres  7840  axpre-suploclemres  7842  axpre-suploc  7843  prime  9290  raluz  9516  indstr  9531  supinfneg  9533  infsupneg  9534  fz1sbc  10031  exbtwnzlemshrink  10184  rebtwn2zlemshrink  10189  apexp1  10631  zfz1iso  10754  caucvgre  10923  maxleast  11155  rexanre  11162  rexico  11163  minmax  11171  xrminmax  11206  addcn2  11251  mulcn2  11253  cn1lem  11255  zsupcllemstep  11878  zsupcllemex  11879  zsupssdc  11887  bezoutlemmain  11931  dfgcd2  11947  exprmfct  12070  prmdvdsexpr  12082  sqrt2irr  12094  pw2dvdslemn  12097  prmpwdvds  12285  infpn2  12389  istopg  12637  lmbr  12853  metcnp  13152  addcncntoplem  13191  2sqlem6  13596  2sqlem8  13599  2sqlem10  13601  bj-rspgt  13667  bdssexg  13786  strcollnft  13866  sscoll2  13870