Theorem imbi1d 230

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 157	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
3	2	imim1d 75	. 2 ⊢ (𝜑 → ((𝜓 → 𝜃) → (𝜒 → 𝜃)))
4	1	biimpd 143	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
5	4	imim1d 75	. 2 ⊢ (𝜑 → ((𝜒 → 𝜃) → (𝜓 → 𝜃)))
6	3, 5	impbid 128	1 ⊢ (𝜑 → ((𝜓 → 𝜃) ↔ (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ↔ wb 104

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  imbi12d  233  imbi1  235  imim21b  251  pm5.33  579  imordc  840  drsb1  1738  ax11v2  1759  ax11v  1766  ax11ev  1767  equs5or  1769  raleqf  2580  rspceaimv  2751  alexeq  2765  mo2icl  2816  sbc19.21g  2929  csbiebg  2992  ralss  3110  ifmdc  3456  ssuni  3705  intmin4  3746  ssexg  4007  pocl  4163  frforeq1  4203  frforeq2  4205  frind  4212  ontr2exmid  4378  elirr  4394  en2lp  4407  tfisi  4439  vtoclr  4525  sosng  4550  fun11  5126  funimass4  5404  dff13  5601  f1mpt  5604  isopolem  5655  oprabid  5735  caovcan  5867  caoftrn  5938  dfsmo2  6114  tfr1onlemsucfn  6167  tfr1onlemsucaccv  6168  tfr1onlembxssdm  6170  tfr1onlembfn  6171  tfr1onlemres  6176  tfrcllemsucfn  6180  tfrcllemsucaccv  6181  tfrcllembxssdm  6183  tfrcllembfn  6184  tfrcllemres  6189  tfrcl  6191  qliftfun  6441  ecoptocl  6446  ecopovtrn  6456  ecopovtrng  6459  dom2lem  6596  ssfiexmid  6699  domfiexmid  6701  findcard  6711  findcard2  6712  findcard2s  6713  fiintim  6746  supmoti  6795  eqsupti  6798  suplubti  6802  supisoex  6811  isomnimap  6921  ismkvmap  6940  ltsonq  7107  prarloclem3  7206  lttrsr  7458  mulextsr1  7476  axpre-lttrn  7569  axpre-mulext  7573  axcaucvglemres  7584  prime  9002  raluz  9223  indstr  9238  supinfneg  9240  infsupneg  9241  fz1sbc  9717  exbtwnzlemshrink  9867  rebtwn2zlemshrink  9872  zfz1iso  10425  caucvgre  10593  maxleast  10825  rexanre  10832  rexico  10833  minmax  10840  xrminmax  10873  addcn2  10918  mulcn2  10920  cn1lem  10922  zsupcllemstep  11433  zsupcllemex  11434  bezoutlemmain  11479  dfgcd2  11495  exprmfct  11611  prmdvdsexpr  11621  sqrt2irr  11633  pw2dvdslemn  11635  istopg  11948  lmbr  12163  metcnp  12436  bj-rspgt  12574  bdssexg  12683