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  613  imordc  904  drsb1  1847  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  cbvabw  2354  raleqf  2726  rspceaimv  2918  alexeq  2932  mo2icl  2985  sbc19.21g  3100  csbcow  3138  csbiebg  3170  ralss  3293  ifmdc  3648  ssuni  3915  intmin4  3956  ssexg  4228  pocl  4400  frforeq1  4440  frforeq2  4442  frind  4449  ontr2exmid  4623  elirr  4639  en2lp  4652  tfisi  4685  vtoclr  4774  sosng  4799  fun11  5397  funimass4  5696  dff13  5908  f1mpt  5911  isopolem  5962  oprabid  6049  caovcan  6186  caoftrn  6267  dfsmo2  6452  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlembfn  6509  tfr1onlemres  6514  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllembfn  6522  tfrcllemres  6527  tfrcl  6529  qliftfun  6785  ecoptocl  6790  ecopovtrn  6800  ecopovtrng  6803  dom2lem  6944  ssfiexmid  7062  ssfiexmidt  7064  domfiexmid  7066  findcard  7076  findcard2  7077  findcard2s  7078  fiintim  7122  supmoti  7191  eqsupti  7194  suplubti  7198  supisoex  7207  isomnimap  7335  ismkvmap  7352  iswomnimap  7364  tapeq1  7470  ltsonq  7617  prarloclem3  7716  suplocexpr  7944  lttrsr  7981  mulextsr1  8000  suplocsrlem  8027  axpre-lttrn  8103  axpre-mulext  8107  axcaucvglemres  8118  axpre-suploclemres  8120  axpre-suploc  8121  prime  9578  raluz  9811  indstr  9826  supinfneg  9828  infsupneg  9829  fz1sbc  10330  zsupcllemstep  10488  zsupcllemex  10489  zsupssdc  10497  exbtwnzlemshrink  10507  rebtwn2zlemshrink  10512  apexp1  10979  zfz1iso  11104  wrdind  11302  wrd2ind  11303  caucvgre  11541  maxleast  11773  rexanre  11780  rexico  11781  minmax  11790  xrminmax  11825  addcn2  11870  mulcn2  11872  cn1lem  11874  bezoutlemmain  12568  dfgcd2  12584  exprmfct  12709  prmdvdsexpr  12721  sqrt2irr  12733  pw2dvdslemn  12736  prmpwdvds  12927  infpn2  13076  isrrg  14276  istopg  14722  lmbr  14936  metcnp  15235  addcncntoplem  15284  mpodvdsmulf1o  15713  lgseisenlem2  15799  2sqlem6  15848  2sqlem8  15851  2sqlem10  15853  bj-rspgt  16382  bdssexg  16499  strcollnft  16579  sscoll2  16583  nnnninfex  16624