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  2710  axextmo  2712  eqeq1dALT  2739  pm13.183  3608  elrab3t  3633  mob  3663  reu6  3672  sbctt  3798  sbcabel  3816  isoeq2  7273  caovcang  7568  caofidlcan  7669  domunfican  9232  axacndlem4  10533  axacnd  10535  expeq0  14054  dfrtrclrec2  15020  relexpind  15026  sumodd  16357  prmdvdsexp  16685  isacs  17617  acsfn  17625  tsrlemax  18552  odeq  19525  isslw  19583  isabv  20788  t0sep  23289  xkopt  23620  kqt0lem  23701  r0sep  23713  nrmr0reg  23714  ismet  24288  isxmet  24289  stdbdxmet  24480  xrsxmet  24775  iccpnfcnv  24911  mdegle0  26042  isppw2  27078  tgjustf  28541  eleclclwwlkn  30146  eupth2lem1  30288  hvaddcan  31141  eigre  31906  opsbc2ie  32545  sgn0bi  32913  xrge0iifcnv  34077  signswch  34705  bnj1468  34988  axsepg2  35225  axsepg2ALT  35226  subtr2  36497  nn0prpwlem  36504  nn0prpw  36505  bj-bm1.3ii  37371  dfgcd3  37638  ftc1anclem6  38019  zindbi  43374  expdioph  43451  islssfg2  43499  eliunov2  44106  pm14.122b  44850  omssaxinf2  45415  permaxrep  45433  permaxsep  45434  permaxinf2lem  45439  permac8prim  45441  elsetpreimafvbi  47851  line2ylem  49227  line2xlem  49229