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  2915  alexeq  2929  mo2icl  2982  sbc19.21g  3097  csbcow  3135  csbiebg  3167  ralss  3290  ifmdc  3645  ssuni  3910  intmin4  3951  ssexg  4223  pocl  4394  frforeq1  4434  frforeq2  4436  frind  4443  ontr2exmid  4617  elirr  4633  en2lp  4646  tfisi  4679  vtoclr  4767  sosng  4792  fun11  5388  funimass4  5686  dff13  5898  f1mpt  5901  isopolem  5952  oprabid  6039  caovcan  6176  caoftrn  6257  dfsmo2  6439  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlembfn  6496  tfr1onlemres  6501  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllembfn  6509  tfrcllemres  6514  tfrcl  6516  qliftfun  6772  ecoptocl  6777  ecopovtrn  6787  ecopovtrng  6790  dom2lem  6931  ssfiexmid  7046  domfiexmid  7048  findcard  7058  findcard2  7059  findcard2s  7060  fiintim  7104  supmoti  7171  eqsupti  7174  suplubti  7178  supisoex  7187  isomnimap  7315  ismkvmap  7332  iswomnimap  7344  tapeq1  7449  ltsonq  7596  prarloclem3  7695  suplocexpr  7923  lttrsr  7960  mulextsr1  7979  suplocsrlem  8006  axpre-lttrn  8082  axpre-mulext  8086  axcaucvglemres  8097  axpre-suploclemres  8099  axpre-suploc  8100  prime  9557  raluz  9785  indstr  9800  supinfneg  9802  infsupneg  9803  fz1sbc  10304  zsupcllemstep  10461  zsupcllemex  10462  zsupssdc  10470  exbtwnzlemshrink  10480  rebtwn2zlemshrink  10485  apexp1  10952  zfz1iso  11076  wrdind  11269  wrd2ind  11270  caucvgre  11507  maxleast  11739  rexanre  11746  rexico  11747  minmax  11756  xrminmax  11791  addcn2  11836  mulcn2  11838  cn1lem  11840  bezoutlemmain  12534  dfgcd2  12550  exprmfct  12675  prmdvdsexpr  12687  sqrt2irr  12699  pw2dvdslemn  12702  prmpwdvds  12893  infpn2  13042  isrrg  14242  istopg  14688  lmbr  14902  metcnp  15201  addcncntoplem  15250  mpodvdsmulf1o  15679  lgseisenlem2  15765  2sqlem6  15814  2sqlem8  15817  2sqlem10  15819  bj-rspgt  16205  bdssexg  16322  strcollnft  16402  sscoll2  16406  nnnninfex  16448