Theorem bibi2d 342

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 337	. . 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 206

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 207

This theorem is referenced by:  bibi1d  343  bibi12d  345  biantr  805  eujust  2571  eujustALT  2572  euf  2576  reu6i  3686  sbc2or  3749  axrep1  5225  axreplem  5226  zfrepclf  5236  axsepg  5242  zfauscl  5243  notzfaus  5308  copsexgw  5438  copsexg  5439  euotd  5461  cnveq0  6155  iota5  6475  eufnfv  7175  isoeq1  7263  isoeq3  7265  isores2  7279  isores3  7281  isotr  7282  isoini2  7285  riota5f  7343  caovordg  7565  caovord  7569  dfoprab4f  8000  seqomlem2  8382  xpf1o  9067  aceq0  10028  dfac5  10039  zfac  10370  zfcndrep  10525  zfcndac  10530  ltasr  11011  axpre-ltadd  11078  absmod0  15226  absz  15234  smuval2  16409  prmdvdsexp  16642  isacs2  17576  isacs1i  17580  mreacs  17581  abvfval  20743  abvpropd  20768  isclo2  23032  t0sep  23268  kqt0lem  23680  r0sep  23692  iccpnfcnv  24898  rolle  25950  2sqreultlem  27414  2sqreunnltlem  27417  tgjustr  28546  wlkeq  29707  eigre  31910  fgreu  32750  fcnvgreu  32751  gsumhashmul  33150  xrge0iifcnv  34090  axsepg2  35238  axsepg2ALT  35239  cvmlift2lem13  35509  iota5f  35918  nn0prpwlem  36516  nn0prpw  36517  bj-zfauscl  37125  wl-eudf  37773  ismndo2  38071  islaut  40339  ispautN  40355  mrefg2  42945  zindbi  43184  jm2.19lem3  43229  oaordnr  43534  omnord1  43543  oenord1  43554  alephiso2  43795  ntrneiel2  44323  ntrneik4  44338  iotavalb  44667  eusnsn  47268  aiota0def  47338  fargshiftfo  47684  isuspgrimlem  48137  line2x  48996  eufsnlem  49082  thincciso  49694  thinccisod  49695  termcarweu  49769