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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1d  346  bibi12d  348  biantr  818  eujust  2598  eujustALT  2599  euf  2603  reu6i  3689  sbc2or  3751  axrep1  5237  axreplem  5238  zfrepclf  5250  axsepg  5256  sepg  5257  zfausclOLD  5259  exnelv  5274  notsep  5332  copsexgw  5470  copsexgwOLD  5471  copsexg  5472  euotd  5494  cnveq0  6195  iota5  6520  eufnfv  7232  isoeq1  7322  isoeq3  7324  isores2  7338  isores3  7340  isotr  7341  isoini2  7344  riota5f  7402  caovordg  7625  caovord  7629  dfoprab4f  8057  seqomlem2  8444  xpf1o  9141  elirrv  9573  aceq0  10125  dfac5  10135  zfac  10466  zfcndrep  10627  zfcndac  10632  ltasr  11113  axpre-ltadd  11180  absmod0  15394  absz  15402  smuval2  16578  prmdvdsexp  16812  isacs2  17747  isacs1i  17751  mreacs  17752  abvfval  20982  abvpropd  21007  isclo2  23319  t0sep  23555  kqt0lem  23968  r0sep  23980  iccpnfcnv  25178  rolle  26224  2sqreultlem  27691  2sqreunnltlem  27694  tgjustr  28823  wlkeq  30101  eigre  32324  fgreu  33152  fcnvgreu  33153  gsumhashmul  33515  xrge0iifcnv  34451  axsepg2  35674  axsepg3  35675  axsepg3ALT  35676  axsepg4  35677  axsepg5  35678  cvmlift2lem13  35902  iota5f  36311  nn0prpwlem  36949  nn0prpw  36950  bj-sepg  37675  bj-inex1gALT  37676  bj-axseprep  37827  bj-axreprepsep  37828  wl-eudf  38343  ismndo2  38632  islaut  40964  ispautN  40980  mrefg2  43560  zindbi  43795  jm2.19lem3  43840  oaordnr  44145  omnord1  44154  oenord1  44165  alephiso2  44406  ntrneiel2  44934  ntrneik4  44949  iotavalb  45262  eusnsn  47922  aiota0def  47992  fargshiftfo  48350  isuspgrimlem  48819  line2x  49692  eufsnlem  49777  thincciso  50387  thinccisod  50388  termcarweu  50462