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  7335  ltsonq  7482  prarloclem3  7581  suplocexpr  7809  lttrsr  7846  mulextsr1  7865  suplocsrlem  7892  axpre-lttrn  7968  axpre-mulext  7972  axcaucvglemres  7983  axpre-suploclemres  7985  axpre-suploc  7986  prime  9442  raluz  9669  indstr  9684  supinfneg  9686  infsupneg  9687  fz1sbc  10188  zsupcllemstep  10336  zsupcllemex  10337  zsupssdc  10345  exbtwnzlemshrink  10355  rebtwn2zlemshrink  10360  apexp1  10827  zfz1iso  10950  caucvgre  11163  maxleast  11395  rexanre  11402  rexico  11403  minmax  11412  xrminmax  11447  addcn2  11492  mulcn2  11494  cn1lem  11496  bezoutlemmain  12190  dfgcd2  12206  exprmfct  12331  prmdvdsexpr  12343  sqrt2irr  12355  pw2dvdslemn  12358  prmpwdvds  12549  infpn2  12698  isrrg  13895  istopg  14319  lmbr  14533  metcnp  14832  addcncntoplem  14881  mpodvdsmulf1o  15310  lgseisenlem2  15396  2sqlem6  15445  2sqlem8  15448  2sqlem10  15450  bj-rspgt  15516  bdssexg  15634  strcollnft  15714  sscoll2  15718