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  2656  eujustALT  2657  euf  2661  reu6i  3721  sbc2or  3783  axrep1  5193  axreplem  5194  zfrepclf  5200  axsepg  5206  zfauscl  5207  notzfaus  5264  copsexgw  5383  copsexg  5384  euotd  5405  cnveq0  6056  iotaval  6331  iota5  6340  eufnfv  6993  isoeq1  7072  isoeq3  7074  isores2  7088  isores3  7090  isotr  7091  isoini2  7094  riota5f  7144  caovordg  7357  caovord  7361  dfoprab4f  7756  seqomlem2  8089  xpf1o  8681  aceq0  9546  dfac5  9556  zfac  9884  zfcndrep  10038  zfcndac  10043  ltasr  10524  axpre-ltadd  10591  absmod0  14665  absz  14673  smuval2  15833  prmdvdsexp  16061  isacs2  16926  isacs1i  16930  mreacs  16931  abvfval  19591  abvpropd  19615  isclo2  21698  t0sep  21934  kqt0lem  22346  r0sep  22358  iccpnfcnv  23550  rolle  24589  2sqreultlem  26025  2sqreunnltlem  26028  tgjustr  26262  wlkeq  27417  eigre  29614  fgreu  30419  fcnvgreu  30420  xrge0iifcnv  31178  cvmlift2lem13  32564  iota5f  32957  nn0prpwlem  33672  nn0prpw  33673  bj-zfauscl  34245  wl-eudf  34810  ismndo2  35154  islaut  37221  ispautN  37237  mrefg2  39311  zindbi  39550  jm2.19lem3  39595  alephiso2  39924  ntrneiel2  40443  ntrneik4  40458  iotavalb  40769  eusnsn  43268  aiota0def  43301  fargshiftfo  43609  line2x  44748