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  2707  axextmo  2709  eqeq1dALT  2736  pm13.183  3617  elrab3t  3642  mob  3672  reu6  3681  sbctt  3807  sbcabel  3825  isoeq2  7258  caovcang  7553  caofidlcan  7654  domunfican  9213  axacndlem4  10508  axacnd  10510  expeq0  14001  dfrtrclrec2  14967  relexpind  14973  sumodd  16301  prmdvdsexp  16628  isacs  17559  acsfn  17567  tsrlemax  18494  odeq  19464  isslw  19522  isabv  20728  t0sep  23240  xkopt  23571  kqt0lem  23652  r0sep  23664  nrmr0reg  23665  ismet  24239  isxmet  24240  stdbdxmet  24431  xrsxmet  24726  iccpnfcnv  24870  mdegle0  26010  isppw2  27053  tgjustf  28452  eleclclwwlkn  30058  eupth2lem1  30200  hvaddcan  31052  eigre  31817  opsbc2ie  32457  sgn0bi  32828  xrge0iifcnv  33967  signswch  34595  bnj1468  34879  axsepg2  35115  axsepg2ALT  35116  subtr2  36380  nn0prpwlem  36387  nn0prpw  36388  bj-bm1.3ii  37129  dfgcd3  37389  ftc1anclem6  37759  zindbi  43064  expdioph  43141  islssfg2  43189  eliunov2  43797  pm14.122b  44541  omssaxinf2  45106  permaxrep  45124  permaxsep  45125  permaxinf2lem  45130  permac8prim  45132  elsetpreimafvbi  47516  line2ylem  48877  line2xlem  48879