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  905  drsb1  1847  ax11v2  1868  ax11v  1875  ax11ev  1876  equs5or  1878  cbvabw  2355  raleqf  2727  rspceaimv  2919  alexeq  2933  mo2icl  2986  sbc19.21g  3101  csbcow  3139  csbiebg  3171  ralss  3294  ifmdc  3652  ssuni  3920  intmin4  3961  ssexg  4233  pocl  4406  frforeq1  4446  frforeq2  4448  frind  4455  ontr2exmid  4629  elirr  4645  en2lp  4658  tfisi  4691  vtoclr  4780  sosng  4805  fun11  5404  funimass4  5705  dff13  5919  f1mpt  5922  isopolem  5973  oprabid  6060  caovcan  6197  caoftrn  6277  dfsmo2  6496  tfr1onlemsucfn  6549  tfr1onlemsucaccv  6550  tfr1onlembxssdm  6552  tfr1onlembfn  6553  tfr1onlemres  6558  tfrcllemsucfn  6562  tfrcllemsucaccv  6563  tfrcllembxssdm  6565  tfrcllembfn  6566  tfrcllemres  6571  tfrcl  6573  qliftfun  6829  ecoptocl  6834  ecopovtrn  6844  ecopovtrng  6847  dom2lem  6988  ssfiexmid  7106  ssfiexmidt  7108  domfiexmid  7110  findcard  7120  findcard2  7121  findcard2s  7122  fiintim  7166  supmoti  7235  eqsupti  7238  suplubti  7242  supisoex  7251  isomnimap  7379  ismkvmap  7396  iswomnimap  7408  tapeq1  7514  ltsonq  7661  prarloclem3  7760  suplocexpr  7988  lttrsr  8025  mulextsr1  8044  suplocsrlem  8071  axpre-lttrn  8147  axpre-mulext  8151  axcaucvglemres  8162  axpre-suploclemres  8164  axpre-suploc  8165  prime  9623  raluz  9856  indstr  9871  supinfneg  9873  infsupneg  9874  fz1sbc  10376  zsupcllemstep  10535  zsupcllemex  10536  zsupssdc  10544  exbtwnzlemshrink  10554  rebtwn2zlemshrink  10559  apexp1  11026  zfz1iso  11151  wrdind  11352  wrd2ind  11353  caucvgre  11604  maxleast  11836  rexanre  11843  rexico  11844  minmax  11853  xrminmax  11888  addcn2  11933  mulcn2  11935  cn1lem  11937  bezoutlemmain  12632  dfgcd2  12648  exprmfct  12773  prmdvdsexpr  12785  sqrt2irr  12797  pw2dvdslemn  12800  prmpwdvds  12991  infpn2  13140  isrrg  14341  istopg  14793  lmbr  15007  metcnp  15306  addcncntoplem  15355  mpodvdsmulf1o  15787  lgseisenlem2  15873  2sqlem6  15922  2sqlem8  15925  2sqlem10  15927  bj-rspgt  16487  bdssexg  16603  strcollnft  16683  sscoll2  16687  exmidcon  16711  exmidpeirce  16712  nnnninfex  16731