Theorem bibi2d 345

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bibi1d  346  bibi12d  348  biantr  804  eujust  2652  eujustALT  2653  euf  2657  reu6i  3718  sbc2or  3780  axrep1  5183  axreplem  5184  zfrepclf  5190  axsepg  5196  zfauscl  5197  notzfaus  5254  copsexgw  5373  copsexg  5374  euotd  5395  cnveq0  6048  iotaval  6323  iota5  6332  eufnfv  6985  isoeq1  7064  isoeq3  7066  isores2  7080  isores3  7082  isotr  7083  isoini2  7086  riota5f  7136  caovordg  7349  caovord  7353  dfoprab4f  7748  seqomlem2  8081  xpf1o  8673  aceq0  9538  dfac5  9548  zfac  9876  zfcndrep  10030  zfcndac  10035  ltasr  10516  axpre-ltadd  10583  absmod0  14657  absz  14665  smuval2  15825  prmdvdsexp  16053  isacs2  16918  isacs1i  16922  mreacs  16923  abvfval  19583  abvpropd  19607  isclo2  21690  t0sep  21926  kqt0lem  22338  r0sep  22350  iccpnfcnv  23542  rolle  24581  2sqreultlem  26017  2sqreunnltlem  26020  tgjustr  26254  wlkeq  27409  eigre  29606  fgreu  30411  fcnvgreu  30412  xrge0iifcnv  31171  cvmlift2lem13  32557  iota5f  32950  nn0prpwlem  33665  nn0prpw  33666  bj-zfauscl  34238  wl-eudf  34802  ismndo2  35146  islaut  37213  ispautN  37229  mrefg2  39297  zindbi  39536  jm2.19lem3  39581  alephiso2  39910  ntrneiel2  40429  ntrneik4  40444  iotavalb  40755  eusnsn  43255  aiota0def  43288  fargshiftfo  43596  line2x  44735