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  883  drsb1  1772  ax11v2  1793  ax11v  1800  ax11ev  1801  equs5or  1803  raleqf  2625  rspceaimv  2801  alexeq  2815  mo2icl  2867  sbc19.21g  2981  csbiebg  3047  ralss  3168  ifmdc  3514  ssuni  3766  intmin4  3807  ssexg  4075  pocl  4233  frforeq1  4273  frforeq2  4275  frind  4282  ontr2exmid  4448  elirr  4464  en2lp  4477  tfisi  4509  vtoclr  4595  sosng  4620  fun11  5198  funimass4  5480  dff13  5677  f1mpt  5680  isopolem  5731  oprabid  5811  caovcan  5943  caoftrn  6015  dfsmo2  6192  tfr1onlemsucfn  6245  tfr1onlemsucaccv  6246  tfr1onlembxssdm  6248  tfr1onlembfn  6249  tfr1onlemres  6254  tfrcllemsucfn  6258  tfrcllemsucaccv  6259  tfrcllembxssdm  6261  tfrcllembfn  6262  tfrcllemres  6267  tfrcl  6269  qliftfun  6519  ecoptocl  6524  ecopovtrn  6534  ecopovtrng  6537  dom2lem  6674  ssfiexmid  6778  domfiexmid  6780  findcard  6790  findcard2  6791  findcard2s  6792  fiintim  6825  supmoti  6888  eqsupti  6891  suplubti  6895  supisoex  6904  isomnimap  7017  ismkvmap  7036  iswomnimap  7048  ltsonq  7230  prarloclem3  7329  suplocexpr  7557  lttrsr  7594  mulextsr1  7613  suplocsrlem  7640  axpre-lttrn  7716  axpre-mulext  7720  axcaucvglemres  7731  axpre-suploclemres  7733  axpre-suploc  7734  prime  9174  raluz  9400  indstr  9415  supinfneg  9417  infsupneg  9418  fz1sbc  9907  exbtwnzlemshrink  10057  rebtwn2zlemshrink  10062  apexp1  10496  zfz1iso  10616  caucvgre  10785  maxleast  11017  rexanre  11024  rexico  11025  minmax  11033  xrminmax  11066  addcn2  11111  mulcn2  11113  cn1lem  11115  zsupcllemstep  11674  zsupcllemex  11675  bezoutlemmain  11722  dfgcd2  11738  exprmfct  11854  prmdvdsexpr  11864  sqrt2irr  11876  pw2dvdslemn  11879  istopg  12205  lmbr  12421  metcnp  12720  addcncntoplem  12759  bj-rspgt  13164  bdssexg  13273  strcollnft  13353  sscoll2  13357