Theorem bibi2d 344

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 272	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 339	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 271	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 271	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 304	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 273	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bibi1d  345  bibi12d  347  biantr  802  eujust  2614  eujustALT  2615  euf  2621  reu6i  3653  sbc2or  3715  axrep1  5082  axreplem  5083  zfrepclf  5089  axsepg  5095  zfauscl  5096  notzfaus  5153  copsexg  5273  euotd  5294  cnveq0  5929  iotaval  6200  iota5  6209  eufnfv  6857  isoeq1  6933  isoeq3  6935  isores2  6949  isores3  6951  isotr  6952  isoini2  6955  riota5f  7002  caovordg  7211  caovord  7215  dfoprab4f  7610  seqomlem2  7938  xpf1o  8526  aceq0  9390  dfac5  9400  zfac  9728  zfcndrep  9882  zfcndac  9887  ltasr  10368  axpre-ltadd  10435  absmod0  14497  absz  14505  smuval2  15664  prmdvdsexp  15888  isacs2  16753  isacs1i  16757  mreacs  16758  abvfval  19279  abvpropd  19303  isclo2  21380  t0sep  21616  kqt0lem  22028  r0sep  22040  iccpnfcnv  23231  rolle  24270  2sqreultlem  25705  2sqreunnltlem  25708  tgjustr  25942  wlkeq  27098  eigre  29303  fgreu  30107  fcnvgreu  30108  xrge0iifcnv  30793  cvmlift2lem13  32170  iota5f  32563  nn0prpwlem  33279  nn0prpw  33280  bj-zfauscl  33814  wl-eudf  34339  ismndo2  34684  islaut  36750  ispautN  36766  mrefg2  38789  zindbi  39028  jm2.19lem3  39073  alephiso2  39402  ntrneiel2  39921  ntrneik4  39936  iotavalb  40300  eusnsn  42777  aiota0def  42810  fargshiftfo  43084  line2x  44222