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  1848  ax11v2  1869  ax11v  1876  ax11ev  1877  equs5or  1879  cbvabw  2359  raleqf  2739  rspceaimv  2932  alexeq  2946  mo2icl  2999  sbc19.21g  3114  csbcow  3152  csbiebg  3184  ralss  3308  ifmdc  3669  ssuni  3941  intmin4  3982  ssexg  4254  pocl  4429  frforeq1  4469  frforeq2  4471  frind  4478  ontr2exmid  4652  elirr  4668  en2lp  4681  tfisi  4714  vtoclr  4803  sosng  4828  fun11  5428  funimass4  5732  dff13  5947  f1mpt  5950  isopolem  6001  oprabid  6090  caovcan  6227  caoftrn  6308  dfsmo2  6531  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlembfn  6588  tfr1onlemres  6593  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllembfn  6601  tfrcllemres  6606  tfrcl  6608  qliftfun  6864  ecoptocl  6869  ecopovtrn  6879  ecopovtrng  6882  dom2lem  7024  ssfiexmid  7144  ssfiexmidt  7146  domfiexmid  7148  findcard  7158  findcard2  7159  findcard2s  7160  fiintim  7204  supmoti  7297  eqsupti  7300  suplubti  7304  supisoex  7313  isomnimap  7441  ismkvmap  7458  iswomnimap  7470  tapeq1  7582  ltsonq  7729  prarloclem3  7828  suplocexpr  8056  lttrsr  8093  mulextsr1  8112  suplocsrlem  8139  axpre-lttrn  8215  axpre-mulext  8219  axcaucvglemres  8230  axpre-suploclemres  8232  axpre-suploc  8233  prime  9695  raluz  9928  indstr  9943  supinfneg  9945  infsupneg  9946  fz1sbc  10452  zsupcllemstep  10611  zsupcllemex  10612  zsupssdc  10622  exbtwnzlemshrink  10632  rebtwn2zlemshrink  10637  apexp1  11105  zfz1iso  11238  wrdind  11439  wrd2ind  11440  caucvgre  11691  maxleast  11923  rexanre  11930  rexico  11931  minmax  11940  xrminmax  11975  addcn2  12020  mulcn2  12022  cn1lem  12024  bezoutlemmain  12719  dfgcd2  12735  exprmfct  12860  prmdvdsexpr  12872  sqrt2irr  12884  pw2dvdslemn  12887  prmpwdvds  13078  infpn2  13291  isrrg  14509  opprdrng  14558  istopg  14990  lmbr  15204  metcnp  15503  addcncntoplem  15552  mpodvdsmulf1o  15984  lgseisenlem2  16070  2sqlem6  16119  2sqlem8  16122  2sqlem10  16124  bj-rspgt  16684  bdssexg  16800  strcollnft  16880  sscoll2  16884  exmidcon  16906  exmidpeirce  16907  nnnninfex  16926