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  27756  wlkeq  28922  eigre  31119  fgreu  31928  fcnvgreu  31929  gsumhashmul  32239  xrge0iifcnv  32944  cvmlift2lem13  34337  iota5f  34724  nn0prpwlem  35255  nn0prpw  35256  bj-zfauscl  35852  wl-eudf  36485  ismndo2  36790  islaut  39002  ispautN  39018  mrefg2  41493  zindbi  41733  jm2.19lem3  41778  oaordnr  42094  omnord1  42103  oenord1  42114  alephiso2  42357  ntrneiel2  42885  ntrneik4  42900  iotavalb  43237  eusnsn  45784  aiota0def  45852  fargshiftfo  46158  line2x  47488  eufsnlem  47555  thincciso  47717