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  609  imordc  899  drsb1  1823  ax11v2  1844  ax11v  1851  ax11ev  1852  equs5or  1854  cbvabw  2330  raleqf  2701  rspceaimv  2892  alexeq  2906  mo2icl  2959  sbc19.21g  3074  csbcow  3112  csbiebg  3144  ralss  3267  ifmdc  3622  ssuni  3886  intmin4  3927  ssexg  4199  pocl  4368  frforeq1  4408  frforeq2  4410  frind  4417  ontr2exmid  4591  elirr  4607  en2lp  4620  tfisi  4653  vtoclr  4741  sosng  4766  fun11  5360  funimass4  5652  dff13  5860  f1mpt  5863  isopolem  5914  oprabid  5999  caovcan  6134  caoftrn  6214  dfsmo2  6396  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlembfn  6453  tfr1onlemres  6458  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllembfn  6466  tfrcllemres  6471  tfrcl  6473  qliftfun  6727  ecoptocl  6732  ecopovtrn  6742  ecopovtrng  6745  dom2lem  6886  ssfiexmid  6999  domfiexmid  7001  findcard  7011  findcard2  7012  findcard2s  7013  fiintim  7054  supmoti  7121  eqsupti  7124  suplubti  7128  supisoex  7137  isomnimap  7265  ismkvmap  7282  iswomnimap  7294  tapeq1  7399  ltsonq  7546  prarloclem3  7645  suplocexpr  7873  lttrsr  7910  mulextsr1  7929  suplocsrlem  7956  axpre-lttrn  8032  axpre-mulext  8036  axcaucvglemres  8047  axpre-suploclemres  8049  axpre-suploc  8050  prime  9507  raluz  9734  indstr  9749  supinfneg  9751  infsupneg  9752  fz1sbc  10253  zsupcllemstep  10409  zsupcllemex  10410  zsupssdc  10418  exbtwnzlemshrink  10428  rebtwn2zlemshrink  10433  apexp1  10900  zfz1iso  11023  wrdind  11213  wrd2ind  11214  caucvgre  11407  maxleast  11639  rexanre  11646  rexico  11647  minmax  11656  xrminmax  11691  addcn2  11736  mulcn2  11738  cn1lem  11740  bezoutlemmain  12434  dfgcd2  12450  exprmfct  12575  prmdvdsexpr  12587  sqrt2irr  12599  pw2dvdslemn  12602  prmpwdvds  12793  infpn2  12942  isrrg  14140  istopg  14586  lmbr  14800  metcnp  15099  addcncntoplem  15148  mpodvdsmulf1o  15577  lgseisenlem2  15663  2sqlem6  15712  2sqlem8  15715  2sqlem10  15717  bj-rspgt  15922  bdssexg  16039  strcollnft  16119  sscoll2  16123  nnnninfex  16161