Theorem bibi1d 343

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 342	. 2 ⊢ (𝜑 → ((𝜃 ↔ 𝜓) ↔ (𝜃 ↔ 𝜒)))
3		bicom 222	. 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓))
4		bicom 222	. 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  bibi12d  345  bibi1  351  biass  384  axextg  2704  axextmo  2706  eqeq1dALT  2733  pm13.183  3635  elrab3t  3661  mob  3691  reu6  3700  sbctt  3826  sbcabel  3844  isoeq2  7296  caovcang  7593  caofidlcan  7694  domunfican  9279  axacndlem4  10570  axacnd  10572  expeq0  14064  dfrtrclrec2  15031  relexpind  15037  sumodd  16365  prmdvdsexp  16692  isacs  17619  acsfn  17627  tsrlemax  18552  odeq  19487  isslw  19545  isabv  20727  t0sep  23218  xkopt  23549  kqt0lem  23630  r0sep  23642  nrmr0reg  23643  ismet  24218  isxmet  24219  stdbdxmet  24410  xrsxmet  24705  iccpnfcnv  24849  mdegle0  25989  isppw2  27032  tgjustf  28407  eleclclwwlkn  30012  eupth2lem1  30154  hvaddcan  31006  eigre  31771  opsbc2ie  32412  sgn0bi  32772  xrge0iifcnv  33930  signswch  34559  bnj1468  34843  axsepg2  35079  axsepg2ALT  35080  subtr2  36310  nn0prpwlem  36317  nn0prpw  36318  bj-bm1.3ii  37059  dfgcd3  37319  ftc1anclem6  37699  zindbi  42942  expdioph  43019  islssfg2  43067  eliunov2  43675  pm14.122b  44419  omssaxinf2  44985  permaxrep  45003  permaxsep  45004  permaxinf2lem  45009  permac8prim  45011  elsetpreimafvbi  47396  line2ylem  48744  line2xlem  48746