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  2564  eujustALT  2565  euf  2569  reu6i  3699  sbc2or  3762  axrep1  5235  axreplem  5236  zfrepclf  5246  axsepg  5252  zfauscl  5253  notzfaus  5318  copsexgw  5450  copsexg  5451  euotd  5473  cnveq0  6170  iotavalOLD  6485  iota5  6494  eufnfv  7203  isoeq1  7292  isoeq3  7294  isores2  7308  isores3  7310  isotr  7311  isoini2  7314  riota5f  7372  caovordg  7596  caovord  7600  dfoprab4f  8035  seqomlem2  8419  xpf1o  9103  aceq0  10071  dfac5  10082  zfac  10413  zfcndrep  10567  zfcndac  10572  ltasr  11053  axpre-ltadd  11120  absmod0  15269  absz  15277  smuval2  16452  prmdvdsexp  16685  isacs2  17614  isacs1i  17618  mreacs  17619  abvfval  20719  abvpropd  20744  isclo2  22975  t0sep  23211  kqt0lem  23623  r0sep  23635  iccpnfcnv  24842  rolle  25894  2sqreultlem  27358  2sqreunnltlem  27361  tgjustr  28401  wlkeq  29562  eigre  31764  fgreu  32596  fcnvgreu  32597  gsumhashmul  33001  xrge0iifcnv  33923  axsepg2  35072  axsepg2ALT  35073  cvmlift2lem13  35302  iota5f  35711  nn0prpwlem  36310  nn0prpw  36311  bj-zfauscl  36912  wl-eudf  37560  ismndo2  37868  islaut  40077  ispautN  40093  mrefg2  42695  zindbi  42935  jm2.19lem3  42980  oaordnr  43285  omnord1  43294  oenord1  43305  alephiso2  43547  ntrneiel2  44075  ntrneik4  44090  iotavalb  44419  eusnsn  47027  aiota0def  47097  fargshiftfo  47443  isuspgrimlem  47895  line2x  48743  eufsnlem  48829  thincciso  49442  thinccisod  49443  termcarweu  49517