Theorem bibi2d 346

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bibi1d  347  bibi12d  349  biantr  805  eujust  2590  eujustALT  2591  euf  2595  reu6i  3642  sbc2or  3705  axrep1  5157  axreplem  5158  zfrepclf  5164  axsepg  5170  zfauscl  5171  notzfaus  5230  copsexgw  5349  copsexg  5350  euotd  5372  cnveq0  6026  iotaval  6309  iota5  6318  eufnfv  6983  isoeq1  7064  isoeq3  7066  isores2  7080  isores3  7082  isotr  7083  isoini2  7086  riota5f  7136  caovordg  7351  caovord  7355  dfoprab4f  7758  seqomlem2  8097  xpf1o  8701  aceq0  9578  dfac5  9588  zfac  9920  zfcndrep  10074  zfcndac  10079  ltasr  10560  axpre-ltadd  10627  absmod0  14711  absz  14719  smuval2  15881  prmdvdsexp  16111  isacs2  16982  isacs1i  16986  mreacs  16987  abvfval  19657  abvpropd  19681  isclo2  21788  t0sep  22024  kqt0lem  22436  r0sep  22448  iccpnfcnv  23645  rolle  24689  2sqreultlem  26130  2sqreunnltlem  26133  tgjustr  26367  wlkeq  27522  eigre  29717  fgreu  30533  fcnvgreu  30534  gsumhashmul  30842  xrge0iifcnv  31404  cvmlift2lem13  32793  iota5f  33187  nn0prpwlem  34060  nn0prpw  34061  bj-zfauscl  34648  wl-eudf  35253  ismndo2  35592  islaut  37659  ispautN  37675  mrefg2  40021  zindbi  40260  jm2.19lem3  40305  alephiso2  40630  ntrneiel2  41162  ntrneik4  41177  iotavalb  41507  eusnsn  43984  aiota0def  44019  fargshiftfo  44327  line2x  45533