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	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
imbi1d	⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Proof of Theorem imbi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimprd 158	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 75	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 144	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 75	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 129	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

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  898  drsb1  1813  ax11v2  1834  ax11v  1841  ax11ev  1842  equs5or  1844  cbvabw  2319  raleqf  2689  rspceaimv  2876  alexeq  2890  mo2icl  2943  sbc19.21g  3058  csbcow  3095  csbiebg  3127  ralss  3250  ifmdc  3602  ssuni  3862  intmin4  3903  ssexg  4173  pocl  4339  frforeq1  4379  frforeq2  4381  frind  4388  ontr2exmid  4562  elirr  4578  en2lp  4591  tfisi  4624  vtoclr  4712  sosng  4737  fun11  5326  funimass4  5614  dff13  5818  f1mpt  5821  isopolem  5872  oprabid  5957  caovcan  6092  caoftrn  6172  dfsmo2  6354  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlembfn  6411  tfr1onlemres  6416  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllembfn  6424  tfrcllemres  6429  tfrcl  6431  qliftfun  6685  ecoptocl  6690  ecopovtrn  6700  ecopovtrng  6703  dom2lem  6840  ssfiexmid  6946  domfiexmid  6948  findcard  6958  findcard2  6959  findcard2s  6960  fiintim  7001  supmoti  7068  eqsupti  7071  suplubti  7075  supisoex  7084  isomnimap  7212  ismkvmap  7229  iswomnimap  7241  tapeq1  7337  ltsonq  7484  prarloclem3  7583  suplocexpr  7811  lttrsr  7848  mulextsr1  7867  suplocsrlem  7894  axpre-lttrn  7970  axpre-mulext  7974  axcaucvglemres  7985  axpre-suploclemres  7987  axpre-suploc  7988  prime  9444  raluz  9671  indstr  9686  supinfneg  9688  infsupneg  9689  fz1sbc  10190  zsupcllemstep  10338  zsupcllemex  10339  zsupssdc  10347  exbtwnzlemshrink  10357  rebtwn2zlemshrink  10362  apexp1  10829  zfz1iso  10952  caucvgre  11165  maxleast  11397  rexanre  11404  rexico  11405  minmax  11414  xrminmax  11449  addcn2  11494  mulcn2  11496  cn1lem  11498  bezoutlemmain  12192  dfgcd2  12208  exprmfct  12333  prmdvdsexpr  12345  sqrt2irr  12357  pw2dvdslemn  12360  prmpwdvds  12551  infpn2  12700  isrrg  13897  istopg  14343  lmbr  14557  metcnp  14856  addcncntoplem  14905  mpodvdsmulf1o  15334  lgseisenlem2  15420  2sqlem6  15469  2sqlem8  15472  2sqlem10  15474  bj-rspgt  15540  bdssexg  15658  strcollnft  15738  sscoll2  15742  nnnninfex  15777