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  7252  eqsupti  7255  suplubti  7259  supisoex  7268  isomnimap  7396  ismkvmap  7413  iswomnimap  7425  tapeq1  7531  ltsonq  7678  prarloclem3  7777  suplocexpr  8005  lttrsr  8042  mulextsr1  8061  suplocsrlem  8088  axpre-lttrn  8164  axpre-mulext  8168  axcaucvglemres  8179  axpre-suploclemres  8181  axpre-suploc  8182  prime  9640  raluz  9873  indstr  9888  supinfneg  9890  infsupneg  9891  fz1sbc  10393  zsupcllemstep  10552  zsupcllemex  10553  zsupssdc  10561  exbtwnzlemshrink  10571  rebtwn2zlemshrink  10576  apexp1  11043  zfz1iso  11168  wrdind  11369  wrd2ind  11370  caucvgre  11621  maxleast  11853  rexanre  11860  rexico  11861  minmax  11870  xrminmax  11905  addcn2  11950  mulcn2  11952  cn1lem  11954  bezoutlemmain  12649  dfgcd2  12665  exprmfct  12790  prmdvdsexpr  12802  sqrt2irr  12814  pw2dvdslemn  12817  prmpwdvds  13008  infpn2  13157  isrrg  14358  istopg  14810  lmbr  15024  metcnp  15323  addcncntoplem  15372  mpodvdsmulf1o  15804  lgseisenlem2  15890  2sqlem6  15939  2sqlem8  15942  2sqlem10  15944  bj-rspgt  16504  bdssexg  16620  strcollnft  16700  sscoll2  16704  exmidcon  16728  exmidpeirce  16729  nnnninfex  16748