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  802  eujust  2571  eujustALT  2572  euf  2576  reu6i  3658  sbc2or  3720  axrep1  5206  axreplem  5207  zfrepclf  5213  axsepg  5219  zfauscl  5220  notzfaus  5280  copsexgw  5398  copsexg  5399  euotd  5421  cnveq0  6089  iotaval  6392  iota5  6401  eufnfv  7087  isoeq1  7168  isoeq3  7170  isores2  7184  isores3  7186  isotr  7187  isoini2  7190  riota5f  7241  caovordg  7457  caovord  7461  dfoprab4f  7869  seqomlem2  8252  xpf1o  8875  aceq0  9805  dfac5  9815  zfac  10147  zfcndrep  10301  zfcndac  10306  ltasr  10787  axpre-ltadd  10854  absmod0  14943  absz  14951  smuval2  16117  prmdvdsexp  16348  isacs2  17279  isacs1i  17283  mreacs  17284  abvfval  19993  abvpropd  20017  isclo2  22147  t0sep  22383  kqt0lem  22795  r0sep  22807  iccpnfcnv  24013  rolle  25059  2sqreultlem  26500  2sqreunnltlem  26503  tgjustr  26739  wlkeq  27903  eigre  30098  fgreu  30911  fcnvgreu  30912  gsumhashmul  31218  xrge0iifcnv  31785  cvmlift2lem13  33177  iota5f  33571  nn0prpwlem  34438  nn0prpw  34439  bj-zfauscl  35039  wl-eudf  35654  ismndo2  35959  islaut  38024  ispautN  38040  mrefg2  40445  zindbi  40684  jm2.19lem3  40729  alephiso2  41054  ntrneiel2  41585  ntrneik4  41600  iotavalb  41937  eusnsn  44407  aiota0def  44475  fargshiftfo  44782  line2x  45988  eufsnlem  46056  thincciso  46218