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 270	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 337	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 269	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 269	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 302	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 271	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bibi1d  343  bibi12d  345  biantr  803  eujust  2569  eujustALT  2570  euf  2574  reu6i  3673  sbc2or  3735  axrep1  5227  axreplem  5228  zfrepclf  5235  axsepg  5241  zfauscl  5242  notzfaus  5302  copsexgw  5428  copsexg  5429  euotd  5451  cnveq0  6129  iotavalOLD  6447  iota5  6456  eufnfv  7155  isoeq1  7238  isoeq3  7240  isores2  7254  isores3  7256  isotr  7257  isoini2  7260  riota5f  7315  caovordg  7533  caovord  7537  dfoprab4f  7956  seqomlem2  8344  xpf1o  8996  aceq0  9967  dfac5  9977  zfac  10309  zfcndrep  10463  zfcndac  10468  ltasr  10949  axpre-ltadd  11016  absmod0  15106  absz  15114  smuval2  16280  prmdvdsexp  16509  isacs2  17451  isacs1i  17455  mreacs  17456  abvfval  20176  abvpropd  20200  isclo2  22337  t0sep  22573  kqt0lem  22985  r0sep  22997  iccpnfcnv  24205  rolle  25252  2sqreultlem  26693  2sqreunnltlem  26696  tgjustr  27037  wlkeq  28203  eigre  30398  fgreu  31209  fcnvgreu  31210  gsumhashmul  31516  xrge0iifcnv  32094  cvmlift2lem13  33489  iota5f  33878  nn0prpwlem  34602  nn0prpw  34603  bj-zfauscl  35202  wl-eudf  35825  ismndo2  36130  islaut  38344  ispautN  38360  mrefg2  40779  zindbi  41019  jm2.19lem3  41064  alephiso2  41475  ntrneiel2  42006  ntrneik4  42021  iotavalb  42358  eusnsn  44860  aiota0def  44928  fargshiftfo  45234  line2x  46440  eufsnlem  46508  thincciso  46670