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  609  imordc  898  drsb1  1821  ax11v2  1842  ax11v  1849  ax11ev  1850  equs5or  1852  cbvabw  2327  raleqf  2697  rspceaimv  2884  alexeq  2898  mo2icl  2951  sbc19.21g  3066  csbcow  3103  csbiebg  3135  ralss  3258  ifmdc  3611  ssuni  3871  intmin4  3912  ssexg  4182  pocl  4348  frforeq1  4388  frforeq2  4390  frind  4397  ontr2exmid  4571  elirr  4587  en2lp  4600  tfisi  4633  vtoclr  4721  sosng  4746  fun11  5335  funimass4  5623  dff13  5827  f1mpt  5830  isopolem  5881  oprabid  5966  caovcan  6101  caoftrn  6181  dfsmo2  6363  tfr1onlemsucfn  6416  tfr1onlemsucaccv  6417  tfr1onlembxssdm  6419  tfr1onlembfn  6420  tfr1onlemres  6425  tfrcllemsucfn  6429  tfrcllemsucaccv  6430  tfrcllembxssdm  6432  tfrcllembfn  6433  tfrcllemres  6438  tfrcl  6440  qliftfun  6694  ecoptocl  6699  ecopovtrn  6709  ecopovtrng  6712  dom2lem  6849  ssfiexmid  6955  domfiexmid  6957  findcard  6967  findcard2  6968  findcard2s  6969  fiintim  7010  supmoti  7077  eqsupti  7080  suplubti  7084  supisoex  7093  isomnimap  7221  ismkvmap  7238  iswomnimap  7250  tapeq1  7346  ltsonq  7493  prarloclem3  7592  suplocexpr  7820  lttrsr  7857  mulextsr1  7876  suplocsrlem  7903  axpre-lttrn  7979  axpre-mulext  7983  axcaucvglemres  7994  axpre-suploclemres  7996  axpre-suploc  7997  prime  9454  raluz  9681  indstr  9696  supinfneg  9698  infsupneg  9699  fz1sbc  10200  zsupcllemstep  10353  zsupcllemex  10354  zsupssdc  10362  exbtwnzlemshrink  10372  rebtwn2zlemshrink  10377  apexp1  10844  zfz1iso  10967  caucvgre  11211  maxleast  11443  rexanre  11450  rexico  11451  minmax  11460  xrminmax  11495  addcn2  11540  mulcn2  11542  cn1lem  11544  bezoutlemmain  12238  dfgcd2  12254  exprmfct  12379  prmdvdsexpr  12391  sqrt2irr  12403  pw2dvdslemn  12406  prmpwdvds  12597  infpn2  12746  isrrg  13943  istopg  14389  lmbr  14603  metcnp  14902  addcncntoplem  14951  mpodvdsmulf1o  15380  lgseisenlem2  15466  2sqlem6  15515  2sqlem8  15518  2sqlem10  15520  bj-rspgt  15586  bdssexg  15704  strcollnft  15784  sscoll2  15788  nnnninfex  15823