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  613  imordc  905  drsb1  1847  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  cbvabw  2355  raleqf  2727  rspceaimv  2919  alexeq  2933  mo2icl  2986  sbc19.21g  3101  csbcow  3139  csbiebg  3171  ralss  3294  ifmdc  3652  ssuni  3920  intmin4  3961  ssexg  4233  pocl  4406  frforeq1  4446  frforeq2  4448  frind  4455  ontr2exmid  4629  elirr  4645  en2lp  4658  tfisi  4691  vtoclr  4780  sosng  4805  fun11  5404  funimass4  5705  dff13  5919  f1mpt  5922  isopolem  5973  oprabid  6060  caovcan  6197  caoftrn  6277  dfsmo2  6496  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemres  6571  tfrcl  6573  qliftfun  6829  ecoptocl  6834  ecopovtrn  6844  ecopovtrng  6847  dom2lem  6988  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  findcard  7120  findcard2  7121  findcard2s  7122  fiintim  7166  supmoti  7235  eqsupti  7238  suplubti  7242  supisoex  7251  isomnimap  7379  ismkvmap  7396  iswomnimap  7408  tapeq1  7514  ltsonq  7661  prarloclem3  7760  suplocexpr  7988  lttrsr  8025  mulextsr1  8044  suplocsrlem  8071  axpre-lttrn  8147  axpre-mulext  8151  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  prime  9622  raluz  9855  indstr  9870  supinfneg  9872  infsupneg  9873  fz1sbc  10374  zsupcllemstep  10533  zsupcllemex  10534  zsupssdc  10542  exbtwnzlemshrink  10552  rebtwn2zlemshrink  10557  apexp1  11024  zfz1iso  11149  wrdind  11350  wrd2ind  11351  caucvgre  11602  maxleast  11834  rexanre  11841  rexico  11842  minmax  11851  xrminmax  11886  addcn2  11931  mulcn2  11933  cn1lem  11935  bezoutlemmain  12630  dfgcd2  12646  exprmfct  12771  prmdvdsexpr  12783  sqrt2irr  12795  pw2dvdslemn  12798  prmpwdvds  12989  infpn2  13138  isrrg  14339  istopg  14790  lmbr  15004  metcnp  15303  addcncntoplem  15352  mpodvdsmulf1o  15781  lgseisenlem2  15867  2sqlem6  15916  2sqlem8  15919  2sqlem10  15921  bj-rspgt  16481  bdssexg  16597  strcollnft  16677  sscoll2  16681  exmidcon  16705  exmidpeirce  16706  nnnninfex  16725