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  2740  axextmo  2742  eqeq1dALT  2769  pm13.183  3628  elrab3t  3652  mob  3683  reu6  3692  sbctt  3816  sbcabel  3834  isoeq2  7327  caovcang  7624  caofidlcan  7725  domunfican  9291  axacndlem4  10613  axacnd  10615  expeq0  14148  dfrtrclrec2  15121  relexpind  15127  sgn0bi  15166  sumodd  16471  prmdvdsexp  16799  isacs  17732  acsfn  17740  tsrlemax  18667  odeq  19651  isslw  19709  isabv  20951  t0sep  23518  xkopt  23849  kqt0lem  23930  r0sep  23942  nrmr0reg  23943  ismet  24517  isxmet  24518  stdbdxmet  24709  xrsxmet  25004  iccpnfcnv  25140  mdegle0  26271  isppw2  27316  tgjustf  28779  eleclclwwlkn  30464  eupth2lem1  30606  hvaddcan  31459  eigre  32224  opsbc2ie  32859  xrge0iifcnv  34354  signswch  34980  bnj1468  35266  axsepg3  35578  axsepg3ALT  35579  axsepg5  35581  subtr2  36867  nn0prpwlem  36874  nn0prpw  36875  bj-bm1.3ii  37741  dfgcd3  38009  ftc1anclem6  38390  zindbi  43714  expdioph  43791  islssfg2  43839  eliunov2  44446  pm14.122b  45174  omssaxinf2  45738  permaxrep  45756  permaxsep  45757  permaxinf2lem  45762  permac8prim  45764  elsetpreimafvbi  48181  line2ylem  49572  line2xlem  49574