Theorem bibi2d 331

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 259	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 326	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 258	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 258	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 291	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 260	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  bibi1d  332  bibi12d  334  biantr  968  bimsc1  976  eujust  2460  eujustALT  2461  euf  2466  reu6i  3364  sbc2or  3411  axrep1  4700  axrep2  4701  axrep3  4702  zfrepclf  4705  axsep2  4710  zfauscl  4711  copsexg  4882  euotd  4900  cnveq0  5509  iotaval  5779  iota5  5788  eufnfv  6395  isoeq1  6467  isoeq3  6469  isores2  6483  isores3  6485  isotr  6486  isoini2  6489  riota5f  6535  caovordg  6739  caovord  6743  dfoprab4f  7117  seqomlem2  7433  xpf1o  8007  aceq0  8824  dfac5  8834  zfac  9165  zfcndrep  9315  zfcndac  9320  ltasr  9800  axpre-ltadd  9867  absmod0  13891  absz  13899  smuval2  15042  prmdvdsexp  15265  isacs2  16137  isacs1i  16141  mreacs  16142  abvfval  18641  abvpropd  18665  isclo2  20702  t0sep  20938  kqt0lem  21349  r0sep  21361  iccpnfcnv  22551  rolle  23557  fargshiftfo  26166  2wlkeq  26235  eigre  28078  fgreu  28854  fcnvgreu  28855  xrge0iifcnv  29307  cvmlift2lem13  30551  iota5f  30861  nn0prpwlem  31487  nn0prpw  31488  bj-axrep1  31976  bj-axrep2  31977  bj-axrep3  31978  bj-axsep2  32113  wl-eudf  32533  ismndo2  32843  islaut  34387  ispautN  34403  mrefg2  36288  zindbi  36529  jm2.19lem3  36576  ntrneiel2  37404  ntrneik4  37419  iotavalb  37653  1wlkeq  40838