Theorem bibi1d 345

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bibi12d  347  bibi1  353  biass  387  axextg  2735  axextmo  2737  eqeq1dALT  2764  pm13.183  3625  elrab3t  3649  mob  3679  reu6  3688  sbctt  3813  sbcabel  3831  isoeq2  7298  caovcang  7593  caofidlcan  7694  domunfican  9262  axacndlem4  10565  axacnd  10567  expeq0  14102  dfrtrclrec2  15068  relexpind  15074  sumodd  16405  prmdvdsexp  16733  isacs  17666  acsfn  17674  tsrlemax  18601  odeq  19573  isslw  19631  isabv  20840  t0sep  23364  xkopt  23695  kqt0lem  23776  r0sep  23788  nrmr0reg  23789  ismet  24363  isxmet  24364  stdbdxmet  24555  xrsxmet  24850  iccpnfcnv  24986  mdegle0  26117  isppw2  27156  tgjustf  28619  eleclclwwlkn  30224  eupth2lem1  30366  hvaddcan  31219  eigre  31984  opsbc2ie  32623  sgn0bi  32992  xrge0iifcnv  34191  signswch  34819  bnj1468  35105  axsepg3  35401  axsepg3ALT  35402  axsepg5  35404  subtr2  36639  nn0prpwlem  36646  nn0prpw  36647  bj-bm1.3ii  37513  dfgcd3  37780  ftc1anclem6  38161  zindbi  43487  expdioph  43564  islssfg2  43612  eliunov2  44219  pm14.122b  44963  omssaxinf2  45528  permaxrep  45546  permaxsep  45547  permaxinf2lem  45552  permac8prim  45554  elsetpreimafvbi  47961  line2ylem  49337  line2xlem  49339