Theorem bibi2d 332

Description: Deduction adding a biconditional to the left in an equivalence. (Contributed by NM, 11-May-1993.) (Proof shortened by Wolf Lammen, 19-May-2013.)

Hypothesis

Ref	Expression
imbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
bibi2d	⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Proof of Theorem bibi2d

Step	Hyp	Ref	Expression
1		imbid.1	. . . . 5 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	pm5.74i 260	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 327	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 259	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 259	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 292	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 261	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  bibi1d  333  bibi12d  335  biantr  972  bimsc1  980  eujust  2472  eujustALT  2473  euf  2478  reu6i  3397  sbc2or  3444  axrep1  4772  axrep2  4773  axrep3  4774  zfrepclf  4777  axsep2  4782  zfauscl  4783  copsexg  4956  euotd  4975  cnveq0  5591  iotaval  5862  iota5  5871  eufnfv  6491  isoeq1  6567  isoeq3  6569  isores2  6583  isores3  6585  isotr  6586  isoini2  6589  riota5f  6636  caovordg  6841  caovord  6845  dfoprab4f  7226  seqomlem2  7546  xpf1o  8122  aceq0  8941  dfac5  8951  zfac  9282  zfcndrep  9436  zfcndac  9441  ltasr  9921  axpre-ltadd  9988  absmod0  14043  absz  14051  smuval2  15204  prmdvdsexp  15427  isacs2  16314  isacs1i  16318  mreacs  16319  abvfval  18818  abvpropd  18842  isclo2  20892  t0sep  21128  kqt0lem  21539  r0sep  21551  iccpnfcnv  22743  rolle  23753  wlkeq  26529  eigre  28694  fgreu  29471  fcnvgreu  29472  xrge0iifcnv  29979  cvmlift2lem13  31297  iota5f  31606  nn0prpwlem  32317  nn0prpw  32318  bj-axrep1  32788  bj-axrep2  32789  bj-axrep3  32790  bj-axsep2  32921  wl-eudf  33354  ismndo2  33673  islaut  35369  ispautN  35385  mrefg2  37270  zindbi  37511  jm2.19lem3  37558  ntrneiel2  38384  ntrneik4  38399  iotavalb  38631  fargshiftfo  41378