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  2571  eujustALT  2572  euf  2576  reu6i  3716  sbc2or  3779  axrep1  5255  axreplem  5256  zfrepclf  5266  axsepg  5272  zfauscl  5273  notzfaus  5338  copsexgw  5470  copsexg  5471  euotd  5493  cnveq0  6191  iotavalOLD  6510  iota5  6519  eufnfv  7226  isoeq1  7315  isoeq3  7317  isores2  7331  isores3  7333  isotr  7334  isoini2  7337  riota5f  7395  caovordg  7619  caovord  7623  dfoprab4f  8060  seqomlem2  8470  xpf1o  9158  aceq0  10137  dfac5  10148  zfac  10479  zfcndrep  10633  zfcndac  10638  ltasr  11119  axpre-ltadd  11186  absmod0  15327  absz  15335  smuval2  16506  prmdvdsexp  16739  isacs2  17670  isacs1i  17674  mreacs  17675  abvfval  20775  abvpropd  20800  isclo2  23031  t0sep  23267  kqt0lem  23679  r0sep  23691  iccpnfcnv  24898  rolle  25951  2sqreultlem  27415  2sqreunnltlem  27418  tgjustr  28458  wlkeq  29619  eigre  31821  fgreu  32655  fcnvgreu  32656  gsumhashmul  33060  xrge0iifcnv  33969  axsepg2  35118  axsepg2ALT  35119  cvmlift2lem13  35342  iota5f  35746  nn0prpwlem  36345  nn0prpw  36346  bj-zfauscl  36947  wl-eudf  37595  ismndo2  37903  islaut  40107  ispautN  40123  mrefg2  42705  zindbi  42945  jm2.19lem3  42990  oaordnr  43295  omnord1  43304  oenord1  43315  alephiso2  43557  ntrneiel2  44085  ntrneik4  44100  iotavalb  44429  eusnsn  47035  aiota0def  47105  fargshiftfo  47436  isuspgrimlem  47888  line2x  48714  eufsnlem  48799  thincciso  49319  thinccisod  49320  termcarweu  49393