Theorem bibi2d 345

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 274	. . . 4 ⊢ ((𝜑 → 𝜓) ↔ (𝜑 → 𝜒))
3	2	bibi2i 340	. . 3 ⊢ (((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
4		pm5.74 273	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜓)))
5		pm5.74 273	. . 3 ⊢ ((𝜑 → (𝜃 ↔ 𝜒)) ↔ ((𝜑 → 𝜃) ↔ (𝜑 → 𝜒)))
6	3, 4, 5	3bitr4i 306	. 2 ⊢ ((𝜑 → (𝜃 ↔ 𝜓)) ↔ (𝜑 → (𝜃 ↔ 𝜒)))
7	6	pm5.74ri 275	1 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi1d  346  bibi12d  348  biantr  818  eujust  2597  eujustALT  2598  euf  2602  reu6i  3686  sbc2or  3748  axrep1  5233  axreplem  5234  zfrepclf  5244  axsepg  5250  sepg  5251  zfausclOLD  5253  exnelv  5267  notsep  5325  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  euotd  5486  cnveq0  6191  iota5  6521  eufnfv  7235  isoeq1  7325  isoeq3  7327  isores2  7341  isores3  7343  isotr  7344  isoini2  7347  riota5f  7405  caovordg  7628  caovord  7632  dfoprab4f  8067  seqomlem2  8461  xpf1o  9158  elirrv  9591  aceq0  10197  dfac5  10207  zfac  10538  zfcndrep  10699  zfcndac  10704  ltasr  11185  axpre-ltadd  11252  absmod0  15470  absz  15478  smuval2  16652  prmdvdsexp  16891  isacs2  17827  isacs1i  17831  mreacs  17832  abvfval  21067  abvpropd  21092  isclo2  23406  t0sep  23642  kqt0lem  24055  r0sep  24067  iccpnfcnv  25265  rolle  26310  2sqreultlem  27774  2sqreunnltlem  27777  tgjustr  28936  wlkeq  30214  eigre  32437  fgreu  33265  fcnvgreu  33266  gsumhashmul  33628  xrge0iifcnv  34565  axsepg2  35808  axsepg3  35809  axsepg3ALT  35810  axsepg4  35811  axsepg5  35812  cvmlift2lem13  36080  iota5f  36489  nn0prpwlem  37110  nn0prpw  37111  bj-sepg  37836  bj-inex1gALT  37837  bj-axseprep  37990  bj-axreprepsep  37991  wl-eudf  38504  ismndo2  38808  islaut  41140  ispautN  41156  mrefg2  43717  zindbi  43952  jm2.19lem3  43997  oaordnr  44297  omnord1  44306  oenord1  44317  alephiso2  44558  ntrneiel2  45085  ntrneik4  45100  iotavalb  45413  eusnsn  48095  aiota0def  48165  fargshiftfo  48523  isuspgrimlem  48992  line2x  49865  eufsnlem  49950  thincciso  50560  thinccisod  50561  termcarweu  50635