Theorem imbi1d 229

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 156	. . 3 |- ( ph -> ( ch -> ps ) )
3	2	imim1d 74	. 2 |- ( ph -> ( ( ps -> th ) -> ( ch -> th ) ) )
4	1	biimpd 142	. . 3 |- ( ph -> ( ps -> ch ) )
5	4	imim1d 74	. 2 |- ( ph -> ( ( ch -> th ) -> ( ps -> th ) ) )
6	3, 5	impbid 127	1 |- ( ph -> ( ( ps -> th ) <-> ( ch -> th ) ) )

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

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  imbi12d  232  imbi1  234  imim21b  250  pm5.33  576  imordc  834  drsb1  1727  ax11v2  1748  ax11v  1755  ax11ev  1756  equs5or  1758  raleqf  2558  alexeq  2741  mo2icl  2792  sbc19.21g  2905  csbiebg  2968  ralss  3085  ifmdc  3424  ssuni  3670  intmin4  3711  ssexg  3970  pocl  4121  frforeq1  4161  frforeq2  4163  frind  4170  ontr2exmid  4331  elirr  4347  en2lp  4360  tfisi  4392  vtoclr  4474  sosng  4499  fun11  5067  funimass4  5339  dff13  5529  f1mpt  5532  isopolem  5583  oprabid  5663  caovcan  5791  caoftrn  5862  dfsmo2  6034  tfr1onlemsucfn  6087  tfr1onlemsucaccv  6088  tfr1onlembxssdm  6090  tfr1onlembfn  6091  tfr1onlemres  6096  tfrcllemsucfn  6100  tfrcllemsucaccv  6101  tfrcllembxssdm  6103  tfrcllembfn  6104  tfrcllemres  6109  tfrcl  6111  qliftfun  6354  ecoptocl  6359  ecopovtrn  6369  ecopovtrng  6372  dom2lem  6469  ssfiexmid  6572  domfiexmid  6574  findcard  6584  findcard2  6585  findcard2s  6586  supmoti  6667  eqsupti  6670  suplubti  6674  supisoex  6683  isomnimap  6772  ltsonq  6936  prarloclem3  7035  lttrsr  7287  mulextsr1  7305  axpre-lttrn  7398  axpre-mulext  7402  axcaucvglemres  7413  prime  8815  raluz  9035  indstr  9050  supinfneg  9052  infsupneg  9053  fz1sbc  9477  exbtwnzlemshrink  9625  rebtwn2zlemshrink  9630  zfz1iso  10210  caucvgre  10378  maxleast  10610  rexanre  10617  rexico  10618  minmax  10624  addcn2  10662  mulcn2  10664  cn1lem  10665  zsupcllemstep  11021  zsupcllemex  11022  bezoutlemmain  11067  dfgcd2  11083  exprmfct  11199  prmdvdsexpr  11209  sqrt2irr  11221  pw2dvdslemn  11223  bj-rspgt  11330  bdssexg  11439