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  3624  elrab3t  3648  mob  3679  reu6  3688  sbctt  3812  sbcabel  3830  isoeq2  7316  caovcang  7613  caofidlcan  7714  domunfican  9279  axacndlem4  10601  axacnd  10603  expeq0  14135  dfrtrclrec2  15102  relexpind  15108  sgn0bi  15147  sumodd  16452  prmdvdsexp  16780  isacs  17713  acsfn  17721  tsrlemax  18648  odeq  19626  isslw  19684  isabv  20925  t0sep  23492  xkopt  23823  kqt0lem  23904  r0sep  23916  nrmr0reg  23917  ismet  24491  isxmet  24492  stdbdxmet  24683  xrsxmet  24978  iccpnfcnv  25114  mdegle0  26245  isppw2  27290  tgjustf  28753  eleclclwwlkn  30438  eupth2lem1  30580  hvaddcan  31433  eigre  32198  opsbc2ie  32833  xrge0iifcnv  34332  signswch  34957  bnj1468  35243  axsepg3  35562  axsepg3ALT  35563  axsepg5  35565  subtr2  36854  nn0prpwlem  36861  nn0prpw  36862  bj-bm1.3ii  37728  dfgcd3  37996  ftc1anclem6  38377  zindbi  43701  expdioph  43778  islssfg2  43826  eliunov2  44433  pm14.122b  45161  omssaxinf2  45725  permaxrep  45743  permaxsep  45744  permaxinf2lem  45749  permac8prim  45751  elsetpreimafvbi  48168  line2ylem  49559  line2xlem  49561