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  7334  eqsupti  7337  suplubti  7341  supisoex  7350  isomnimap  7478  ismkvmap  7495  iswomnimap  7507  tapeq1  7619  ltsonq  7766  prarloclem3  7865  suplocexpr  8093  lttrsr  8130  mulextsr1  8149  suplocsrlem  8176  axpre-lttrn  8252  axpre-mulext  8256  axcaucvglemres  8267  axpre-suploclemres  8269  axpre-suploc  8270  prime  9750  raluz  9988  indstr  10003  supinfneg  10005  infsupneg  10006  fz1sbc  10514  zsupcllemstep  10673  zsupcllemex  10674  zsupssdc  10684  exbtwnzlemshrink  10694  rebtwn2zlemshrink  10699  apexp1  11172  zfz1iso  11309  wrdind  11510  wrd2ind  11511  caucvgre  11763  maxleast  11996  rexanre  12003  rexico  12004  minmax  12014  xrminmax  12050  addcn2  12095  mulcn2  12097  cn1lem  12099  bezoutlemmain  12794  dfgcd2  12810  exprmfct  12936  prmdvdsexpr  12948  sqrt2irr  12960  pwbdvdslemn  12963  prmpwdvds  13157  infpn2  13399  isrrg  14655  opprdrng  14704  istopg  15191  lmbr  15405  metcnp  15704  addcncntoplem  15753  mpodvdsmulf1o  16245  ppiublem1  16252  lgseisenlem2  16356  2sqlem6  16405  2sqlem8  16408  2sqlem10  16410  bj-rspgt  16980  bdssexg  17096  strcollnft  17176  sscoll2  17180  exmidcon  17203  exmidpeirce  17204  nnnninfex  17231