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  613  imordc  904  drsb1  1847  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  cbvabw  2354  raleqf  2726  rspceaimv  2918  alexeq  2932  mo2icl  2985  sbc19.21g  3100  csbcow  3138  csbiebg  3170  ralss  3293  ifmdc  3648  ssuni  3915  intmin4  3956  ssexg  4228  pocl  4400  frforeq1  4440  frforeq2  4442  frind  4449  ontr2exmid  4623  elirr  4639  en2lp  4652  tfisi  4685  vtoclr  4774  sosng  4799  fun11  5397  funimass4  5696  dff13  5909  f1mpt  5912  isopolem  5963  oprabid  6050  caovcan  6187  caoftrn  6268  dfsmo2  6453  tfr1onlemsucfn  6506  tfr1onlemsucaccv  6507  tfr1onlembxssdm  6509  tfr1onlembfn  6510  tfr1onlemres  6515  tfrcllemsucfn  6519  tfrcllemsucaccv  6520  tfrcllembxssdm  6522  tfrcllembfn  6523  tfrcllemres  6528  tfrcl  6530  qliftfun  6786  ecoptocl  6791  ecopovtrn  6801  ecopovtrng  6804  dom2lem  6945  ssfiexmid  7063  ssfiexmidt  7065  domfiexmid  7067  findcard  7077  findcard2  7078  findcard2s  7079  fiintim  7123  supmoti  7192  eqsupti  7195  suplubti  7199  supisoex  7208  isomnimap  7336  ismkvmap  7353  iswomnimap  7365  tapeq1  7471  ltsonq  7618  prarloclem3  7717  suplocexpr  7945  lttrsr  7982  mulextsr1  8001  suplocsrlem  8028  axpre-lttrn  8104  axpre-mulext  8108  axcaucvglemres  8119  axpre-suploclemres  8121  axpre-suploc  8122  prime  9579  raluz  9812  indstr  9827  supinfneg  9829  infsupneg  9830  fz1sbc  10331  zsupcllemstep  10490  zsupcllemex  10491  zsupssdc  10499  exbtwnzlemshrink  10509  rebtwn2zlemshrink  10514  apexp1  10981  zfz1iso  11106  wrdind  11307  wrd2ind  11308  caucvgre  11546  maxleast  11778  rexanre  11785  rexico  11786  minmax  11795  xrminmax  11830  addcn2  11875  mulcn2  11877  cn1lem  11879  bezoutlemmain  12574  dfgcd2  12590  exprmfct  12715  prmdvdsexpr  12727  sqrt2irr  12739  pw2dvdslemn  12742  prmpwdvds  12933  infpn2  13082  isrrg  14283  istopg  14729  lmbr  14943  metcnp  15242  addcncntoplem  15291  mpodvdsmulf1o  15720  lgseisenlem2  15806  2sqlem6  15855  2sqlem8  15858  2sqlem10  15860  bj-rspgt  16408  bdssexg  16525  strcollnft  16605  sscoll2  16609  nnnninfex  16650