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  4272  pocl  4448  frforeq1  4488  frforeq2  4490  frind  4497  ontr2exmid  4672  elirr  4688  en2lp  4701  tfisi  4734  vtoclr  4823  sosng  4848  fun11  5448  funimass4  5753  dff13  5974  f1mpt  5977  isopolem  6028  oprabid  6117  caovcan  6254  caoftrn  6335  dfsmo2  6558  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlembfn  6615  tfr1onlemres  6620  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllembfn  6628  tfrcllemres  6633  tfrcl  6635  qliftfun  6891  ecoptocl  6896  ecopovtrn  6906  ecopovtrng  6909  dom2lem  7058  ssfiexmid  7178  ssfiexmidt  7180  domfiexmid  7182  findcard  7192  findcard2  7193  findcard2s  7194  fiintim  7238  supmoti  7333  eqsupti  7336  suplubti  7340  supisoex  7349  isomnimap  7477  ismkvmap  7494  iswomnimap  7506  tapeq1  7618  ltsonq  7765  prarloclem3  7864  suplocexpr  8092  lttrsr  8129  mulextsr1  8148  suplocsrlem  8175  axpre-lttrn  8251  axpre-mulext  8255  axcaucvglemres  8266  axpre-suploclemres  8268  axpre-suploc  8269  prime  9749  raluz  9987  indstr  10002  supinfneg  10004  infsupneg  10005  fz1sbc  10513  zsupcllemstep  10672  zsupcllemex  10673  zsupssdc  10683  exbtwnzlemshrink  10693  rebtwn2zlemshrink  10698  apexp1  11170  zfz1iso  11307  wrdind  11508  wrd2ind  11509  caucvgre  11761  maxleast  11994  rexanre  12001  rexico  12002  minmax  12011  xrminmax  12047  addcn2  12092  mulcn2  12094  cn1lem  12096  bezoutlemmain  12791  dfgcd2  12807  exprmfct  12933  prmdvdsexpr  12945  sqrt2irr  12957  pwbdvdslemn  12960  prmpwdvds  13154  infpn2  13396  isrrg  14620  opprdrng  14669  istopg  15149  lmbr  15363  metcnp  15662  addcncntoplem  15711  mpodvdsmulf1o  16185  ppiublem1  16192  lgseisenlem2  16288  2sqlem6  16337  2sqlem8  16340  2sqlem10  16342  bj-rspgt  16912  bdssexg  17028  strcollnft  17108  sscoll2  17112  exmidcon  17135  exmidpeirce  17136  nnnninfex  17163