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  2568  eujustALT  2569  euf  2573  reu6i  3683  sbc2or  3746  axrep1  5220  axreplem  5221  zfrepclf  5231  axsepg  5237  zfauscl  5238  notzfaus  5303  copsexgw  5433  copsexg  5434  euotd  5456  cnveq0  6149  iota5  6469  eufnfv  7169  isoeq1  7257  isoeq3  7259  isores2  7273  isores3  7275  isotr  7276  isoini2  7279  riota5f  7337  caovordg  7559  caovord  7563  dfoprab4f  7994  seqomlem2  8376  xpf1o  9059  aceq0  10016  dfac5  10027  zfac  10358  zfcndrep  10512  zfcndac  10517  ltasr  10998  axpre-ltadd  11065  absmod0  15212  absz  15220  smuval2  16395  prmdvdsexp  16628  isacs2  17561  isacs1i  17565  mreacs  17566  abvfval  20727  abvpropd  20752  isclo2  23004  t0sep  23240  kqt0lem  23652  r0sep  23664  iccpnfcnv  24870  rolle  25922  2sqreultlem  27386  2sqreunnltlem  27389  tgjustr  28453  wlkeq  29614  eigre  31817  fgreu  32656  fcnvgreu  32657  gsumhashmul  33048  xrge0iifcnv  33967  axsepg2  35115  axsepg2ALT  35116  cvmlift2lem13  35380  iota5f  35789  nn0prpwlem  36387  nn0prpw  36388  bj-zfauscl  36989  wl-eudf  37637  ismndo2  37934  islaut  40202  ispautN  40218  mrefg2  42824  zindbi  43063  jm2.19lem3  43108  oaordnr  43413  omnord1  43422  oenord1  43433  alephiso2  43675  ntrneiel2  44203  ntrneik4  44218  iotavalb  44547  eusnsn  47150  aiota0def  47220  fargshiftfo  47566  isuspgrimlem  48019  line2x  48879  eufsnlem  48965  thincciso  49578  thinccisod  49579  termcarweu  49653