Theorem bibi1d 346

Description: Deduction adding a biconditional to the right in an equivalence. (Contributed by NM, 11-May-1993.)

Hypothesis

Ref	Expression
imbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
bibi1d	⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))

Proof of Theorem bibi1d

Step	Hyp	Ref	Expression
1		imbid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	bibi2d 345	. 2 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))
3		bicom 225	. 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓))
4		bicom 225	. 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒))
5	2, 3, 4	3bitr4g 317	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:  bibi12d  348  bibi1  354  biass  388  axextg  2736  axextmo  2738  eqeq1dALT  2765  pm13.183  3623  elrab3t  3647  mob  3678  reu6  3687  sbctt  3811  sbcabel  3828  isoeq2  7323  caovcang  7619  caofidlcan  7720  domunfican  9295  axacndlem4  10623  axacnd  10625  expeq0  14160  dfrtrclrec2  15135  relexpind  15141  sgn0bi  15180  sumodd  16484  prmdvdsexp  16812  isacs  17745  acsfn  17753  tsrlemax  18680  odeq  19683  isslw  19741  isabv  20983  t0sep  23555  xkopt  23887  kqt0lem  23968  r0sep  23980  nrmr0reg  23981  ismet  24555  isxmet  24556  stdbdxmet  24747  xrsxmet  25042  iccpnfcnv  25178  mdegle0  26309  isppw2  27359  tgjustf  28822  eleclclwwlkn  30554  eupth2lem1  30706  hvaddcan  31559  eigre  32324  opsbc2ie  32959  xrge0iifcnv  34451  signswch  35077  bnj1468  35363  axsepg3  35675  axsepg3ALT  35676  axsepg5  35678  subtr2  36942  nn0prpwlem  36949  nn0prpw  36950  bj-bm1.3ii  37816  dfgcd3  38084  ftc1anclem6  38455  zindbi  43795  expdioph  43872  islssfg2  43920  eliunov2  44527  pm14.122b  45255  omssaxinf2  45819  permaxrep  45837  permaxsep  45838  permaxinf2lem  45843  permac8prim  45845  elsetpreimafvbi  48299  line2ylem  49689  line2xlem  49691