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  9745  raluz  9978  indstr  9993  supinfneg  9995  infsupneg  9996  fz1sbc  10503  zsupcllemstep  10662  zsupcllemex  10663  zsupssdc  10673  exbtwnzlemshrink  10683  rebtwn2zlemshrink  10688  apexp1  11156  zfz1iso  11293  wrdind  11494  wrd2ind  11495  caucvgre  11747  maxleast  11979  rexanre  11986  rexico  11987  minmax  11996  xrminmax  12031  addcn2  12076  mulcn2  12078  cn1lem  12080  bezoutlemmain  12775  dfgcd2  12791  exprmfct  12916  prmdvdsexpr  12928  sqrt2irr  12940  pw2dvdslemn  12943  prmpwdvds  13134  infpn2  13347  isrrg  14571  opprdrng  14620  istopg  15100  lmbr  15314  metcnp  15613  addcncntoplem  15662  mpodvdsmulf1o  16104  lgseisenlem2  16190  2sqlem6  16239  2sqlem8  16242  2sqlem10  16244  bj-rspgt  16814  bdssexg  16930  strcollnft  17010  sscoll2  17014  exmidcon  17037  exmidpeirce  17038  nnnninfex  17065