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

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  imbi12d  234  imbi1  236  imim21b  253  pm5.33  617  imordc  909  drsb1  1852  ax11v2  1873  ax11v  1880  ax11ev  1881  equs5or  1883  cbvabw  2363  raleqf  2745  rspceaimv  2938  alexeq  2952  mo2icl  3005  sbc19.21g  3120  csbcow  3158  csbiebg  3190  ralss  3314  ifmdc  3683  ssuni  3957  intmin4  3998  ssexg  4274  pocl  4450  frforeq1  4490  frforeq2  4492  frind  4499  ontr2exmid  4674  elirr  4690  en2lp  4703  tfisi  4736  vtoclr  4825  sosng  4850  fun11  5451  funimass4  5756  dff13  5977  f1mpt  5980  isopolem  6031  oprabid  6120  caovcan  6257  caoftrn  6339  dfsmo2  6563  tfr1onlemsucfn  6616  tfr1onlemsucaccv  6617  tfr1onlembxssdm  6619  tfr1onlembfn  6620  tfr1onlemres  6625  tfrcllemsucfn  6629  tfrcllemsucaccv  6630  tfrcllembxssdm  6632  tfrcllembfn  6633  tfrcllemres  6638  tfrcl  6640  qliftfun  6896  ecoptocl  6901  ecopovtrn  6911  ecopovtrng  6914  dom2lem  7064  ssfiexmid  7184  ssfiexmidt  7186  domfiexmid  7188  findcard  7198  findcard2  7199  findcard2s  7200  fiintim  7244  supmoti  7339  eqsupti  7342  suplubti  7346  supisoex  7355  isomnimap  7483  ismkvmap  7500  iswomnimap  7512  tapeq1  7624  ltsonq  7771  prarloclem3  7870  suplocexpr  8098  lttrsr  8135  mulextsr1  8154  suplocsrlem  8181  axpre-lttrn  8257  axpre-mulext  8261  axcaucvglemres  8272  axpre-suploclemres  8274  axpre-suploc  8275  prime  9755  raluz  9993  indstr  10008  supinfneg  10010  infsupneg  10011  fz1sbc  10519  zsupcllemstep  10678  zsupcllemex  10679  zsupssdc  10689  exbtwnzlemshrink  10699  rebtwn2zlemshrink  10704  apexp1  11177  zfz1iso  11314  wrdind  11515  wrd2ind  11516  caucvgre  11768  maxleast  12001  rexanre  12008  rexico  12009  minmax  12019  xrminmax  12055  addcn2  12100  mulcn2  12102  cn1lem  12104  bezoutlemmain  12799  dfgcd2  12815  exprmfct  12941  prmdvdsexpr  12953  sqrt2irr  12965  pwbdvdslemn  12968  prmpwdvds  13162  infpn2  13404  isrrg  14679  opprdrng  14728  istopg  15242  lmbr  15456  metcnp  15755  addcncntoplem  15804  mpodvdsmulf1o  16301  ppiublem1  16308  lgseisenlem2  16412  2sqlem6  16461  2sqlem8  16464  2sqlem10  16466  bj-rspgt  17036  bdssexg  17152  strcollnft  17232  sscoll2  17236  exmidcon  17259  exmidpeirce  17260  nnnninfex  17288