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  611  imordc  902  drsb1  1845  ax11v2  1866  ax11v  1873  ax11ev  1874  equs5or  1876  cbvabw  2352  raleqf  2724  rspceaimv  2916  alexeq  2930  mo2icl  2983  sbc19.21g  3098  csbcow  3136  csbiebg  3168  ralss  3291  ifmdc  3646  ssuni  3913  intmin4  3954  ssexg  4226  pocl  4398  frforeq1  4438  frforeq2  4440  frind  4447  ontr2exmid  4621  elirr  4637  en2lp  4650  tfisi  4683  vtoclr  4772  sosng  4797  fun11  5394  funimass4  5692  dff13  5904  f1mpt  5907  isopolem  5958  oprabid  6045  caovcan  6182  caoftrn  6263  dfsmo2  6448  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlembfn  6505  tfr1onlemres  6510  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllembfn  6518  tfrcllemres  6523  tfrcl  6525  qliftfun  6781  ecoptocl  6786  ecopovtrn  6796  ecopovtrng  6799  dom2lem  6940  ssfiexmid  7058  domfiexmid  7060  findcard  7070  findcard2  7071  findcard2s  7072  fiintim  7116  supmoti  7183  eqsupti  7186  suplubti  7190  supisoex  7199  isomnimap  7327  ismkvmap  7344  iswomnimap  7356  tapeq1  7461  ltsonq  7608  prarloclem3  7707  suplocexpr  7935  lttrsr  7972  mulextsr1  7991  suplocsrlem  8018  axpre-lttrn  8094  axpre-mulext  8098  axcaucvglemres  8109  axpre-suploclemres  8111  axpre-suploc  8112  prime  9569  raluz  9802  indstr  9817  supinfneg  9819  infsupneg  9820  fz1sbc  10321  zsupcllemstep  10479  zsupcllemex  10480  zsupssdc  10488  exbtwnzlemshrink  10498  rebtwn2zlemshrink  10503  apexp1  10970  zfz1iso  11095  wrdind  11293  wrd2ind  11294  caucvgre  11532  maxleast  11764  rexanre  11771  rexico  11772  minmax  11781  xrminmax  11816  addcn2  11861  mulcn2  11863  cn1lem  11865  bezoutlemmain  12559  dfgcd2  12575  exprmfct  12700  prmdvdsexpr  12712  sqrt2irr  12724  pw2dvdslemn  12727  prmpwdvds  12918  infpn2  13067  isrrg  14267  istopg  14713  lmbr  14927  metcnp  15226  addcncntoplem  15275  mpodvdsmulf1o  15704  lgseisenlem2  15790  2sqlem6  15839  2sqlem8  15842  2sqlem10  15844  bj-rspgt  16318  bdssexg  16435  strcollnft  16515  sscoll2  16519  nnnninfex  16560