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  804  eujust  2564  eujustALT  2565  euf  2569  reu6i  3689  sbc2or  3751  axrep1  5248  axreplem  5249  zfrepclf  5256  axsepg  5262  zfauscl  5263  notzfaus  5323  copsexgw  5452  copsexg  5453  euotd  5475  cnveq0  6154  iotavalOLD  6475  iota5  6484  eufnfv  7184  isoeq1  7267  isoeq3  7269  isores2  7283  isores3  7285  isotr  7286  isoini2  7289  riota5f  7347  caovordg  7566  caovord  7570  dfoprab4f  7993  seqomlem2  8402  xpf1o  9090  aceq0  10063  dfac5  10073  zfac  10405  zfcndrep  10559  zfcndac  10564  ltasr  11045  axpre-ltadd  11112  absmod0  15200  absz  15208  smuval2  16373  prmdvdsexp  16602  isacs2  17547  isacs1i  17551  mreacs  17552  abvfval  20333  abvpropd  20357  isclo2  22476  t0sep  22712  kqt0lem  23124  r0sep  23136  iccpnfcnv  24344  rolle  25391  2sqreultlem  26832  2sqreunnltlem  26835  tgjustr  27479  wlkeq  28645  eigre  30840  fgreu  31655  fcnvgreu  31656  gsumhashmul  31968  xrge0iifcnv  32603  cvmlift2lem13  33996  iota5f  34382  nn0prpwlem  34870  nn0prpw  34871  bj-zfauscl  35467  wl-eudf  36100  ismndo2  36406  islaut  38619  ispautN  38635  mrefg2  41088  zindbi  41328  jm2.19lem3  41373  oaordnr  41689  omnord1  41698  oenord1  41709  alephiso2  41952  ntrneiel2  42480  ntrneik4  42495  iotavalb  42832  eusnsn  45380  aiota0def  45448  fargshiftfo  45754  line2x  46960  eufsnlem  47027  thincciso  47189