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  2566  eujustALT  2567  euf  2571  reu6i  3687  sbc2or  3750  axrep1  5218  axreplem  5219  zfrepclf  5229  axsepg  5235  zfauscl  5236  notzfaus  5301  copsexgw  5430  copsexg  5431  euotd  5453  cnveq0  6144  iota5  6464  eufnfv  7163  isoeq1  7251  isoeq3  7253  isores2  7267  isores3  7269  isotr  7270  isoini2  7273  riota5f  7331  caovordg  7553  caovord  7557  dfoprab4f  7988  seqomlem2  8370  xpf1o  9052  aceq0  10006  dfac5  10017  zfac  10348  zfcndrep  10502  zfcndac  10507  ltasr  10988  axpre-ltadd  11055  absmod0  15207  absz  15215  smuval2  16390  prmdvdsexp  16623  isacs2  17556  isacs1i  17560  mreacs  17561  abvfval  20723  abvpropd  20748  isclo2  23001  t0sep  23237  kqt0lem  23649  r0sep  23661  iccpnfcnv  24867  rolle  25919  2sqreultlem  27383  2sqreunnltlem  27386  tgjustr  28450  wlkeq  29610  eigre  31810  fgreu  32649  fcnvgreu  32650  gsumhashmul  33036  xrge0iifcnv  33941  axsepg2  35089  axsepg2ALT  35090  cvmlift2lem13  35347  iota5f  35756  nn0prpwlem  36355  nn0prpw  36356  bj-zfauscl  36957  wl-eudf  37605  ismndo2  37913  islaut  40121  ispautN  40137  mrefg2  42739  zindbi  42978  jm2.19lem3  43023  oaordnr  43328  omnord1  43337  oenord1  43348  alephiso2  43590  ntrneiel2  44118  ntrneik4  44133  iotavalb  44462  eusnsn  47056  aiota0def  47126  fargshiftfo  47472  isuspgrimlem  47925  line2x  48785  eufsnlem  48871  thincciso  49484  thinccisod  49485  termcarweu  49559