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  899  drsb1  1823  ax11v2  1844  ax11v  1851  ax11ev  1852  equs5or  1854  cbvabw  2329  raleqf  2699  rspceaimv  2889  alexeq  2903  mo2icl  2956  sbc19.21g  3071  csbcow  3108  csbiebg  3140  ralss  3263  ifmdc  3617  ssuni  3878  intmin4  3919  ssexg  4191  pocl  4358  frforeq1  4398  frforeq2  4400  frind  4407  ontr2exmid  4581  elirr  4597  en2lp  4610  tfisi  4643  vtoclr  4731  sosng  4756  fun11  5350  funimass4  5642  dff13  5850  f1mpt  5853  isopolem  5904  oprabid  5989  caovcan  6124  caoftrn  6204  dfsmo2  6386  tfr1onlemsucfn  6439  tfr1onlemsucaccv  6440  tfr1onlembxssdm  6442  tfr1onlembfn  6443  tfr1onlemres  6448  tfrcllemsucfn  6452  tfrcllemsucaccv  6453  tfrcllembxssdm  6455  tfrcllembfn  6456  tfrcllemres  6461  tfrcl  6463  qliftfun  6717  ecoptocl  6722  ecopovtrn  6732  ecopovtrng  6735  dom2lem  6876  ssfiexmid  6988  domfiexmid  6990  findcard  7000  findcard2  7001  findcard2s  7002  fiintim  7043  supmoti  7110  eqsupti  7113  suplubti  7117  supisoex  7126  isomnimap  7254  ismkvmap  7271  iswomnimap  7283  tapeq1  7384  ltsonq  7531  prarloclem3  7630  suplocexpr  7858  lttrsr  7895  mulextsr1  7914  suplocsrlem  7941  axpre-lttrn  8017  axpre-mulext  8021  axcaucvglemres  8032  axpre-suploclemres  8034  axpre-suploc  8035  prime  9492  raluz  9719  indstr  9734  supinfneg  9736  infsupneg  9737  fz1sbc  10238  zsupcllemstep  10394  zsupcllemex  10395  zsupssdc  10403  exbtwnzlemshrink  10413  rebtwn2zlemshrink  10418  apexp1  10885  zfz1iso  11008  wrdind  11198  wrd2ind  11199  caucvgre  11367  maxleast  11599  rexanre  11606  rexico  11607  minmax  11616  xrminmax  11651  addcn2  11696  mulcn2  11698  cn1lem  11700  bezoutlemmain  12394  dfgcd2  12410  exprmfct  12535  prmdvdsexpr  12547  sqrt2irr  12559  pw2dvdslemn  12562  prmpwdvds  12753  infpn2  12902  isrrg  14100  istopg  14546  lmbr  14760  metcnp  15059  addcncntoplem  15108  mpodvdsmulf1o  15537  lgseisenlem2  15623  2sqlem6  15672  2sqlem8  15675  2sqlem10  15677  bj-rspgt  15861  bdssexg  15978  strcollnft  16058  sscoll2  16062  nnnninfex  16100