Theorem bibi2d 343

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bibi1d  344  bibi12d  346  biantr  805  eujust  2566  eujustALT  2567  euf  2571  reu6i  3725  sbc2or  3787  axrep1  5287  axreplem  5288  zfrepclf  5295  axsepg  5301  zfauscl  5302  notzfaus  5362  copsexgw  5491  copsexg  5492  euotd  5514  cnveq0  6197  iotavalOLD  6518  iota5  6527  eufnfv  7231  isoeq1  7314  isoeq3  7316  isores2  7330  isores3  7332  isotr  7333  isoini2  7336  riota5f  7394  caovordg  7614  caovord  7618  dfoprab4f  8042  seqomlem2  8451  xpf1o  9139  aceq0  10113  dfac5  10123  zfac  10455  zfcndrep  10609  zfcndac  10614  ltasr  11095  axpre-ltadd  11162  absmod0  15250  absz  15258  smuval2  16423  prmdvdsexp  16652  isacs2  17597  isacs1i  17601  mreacs  17602  abvfval  20426  abvpropd  20450  isclo2  22592  t0sep  22828  kqt0lem  23240  r0sep  23252  iccpnfcnv  24460  rolle  25507  2sqreultlem  26950  2sqreunnltlem  26953  tgjustr  27725  wlkeq  28891  eigre  31088  fgreu  31897  fcnvgreu  31898  gsumhashmul  32208  xrge0iifcnv  32913  cvmlift2lem13  34306  iota5f  34693  nn0prpwlem  35207  nn0prpw  35208  bj-zfauscl  35804  wl-eudf  36437  ismndo2  36742  islaut  38954  ispautN  38970  mrefg2  41445  zindbi  41685  jm2.19lem3  41730  oaordnr  42046  omnord1  42055  oenord1  42066  alephiso2  42309  ntrneiel2  42837  ntrneik4  42852  iotavalb  43189  eusnsn  45736  aiota0def  45804  fargshiftfo  46110  line2x  47440  eufsnlem  47507  thincciso  47669