Theorem bibi1d 332

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

Syntax hints:   → wi 4   ↔ wb 196

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 197

This theorem is referenced by:  bibi12d  334  bibi1  340  biass  373  eubid  2625  axext3  2742  axext3ALT  2743  bm1.1  2745  eqeq1dALT  2763  pm13.183  3484  elabgt  3487  elrab3t  3503  mob  3529  reu6  3536  sbctt  3641  sbcabel  3658  isoeq2  6731  caovcang  7000  domunfican  8398  axacndlem4  9624  axacnd  9626  expeq0  13084  dfrtrclrec2  13996  relexpind  14003  sumodd  15313  prmdvdsexp  15629  isacs  16513  acsfn  16521  tsrlemax  17421  odeq  18169  isslw  18223  isabv  19021  t0sep  21330  xkopt  21660  kqt0lem  21741  r0sep  21753  nrmr0reg  21754  ismet  22329  isxmet  22330  stdbdxmet  22521  xrsxmet  22813  iccpnfcnv  22944  mdegle0  24036  isppw2  25040  eleclclwwlkn  27207  eupth2lem1  27370  hvaddcan  28236  eigre  29003  xrge0iifcnv  30288  sgn0bi  30918  signswch  30947  bnj1468  31223  br1steqgOLD  31979  br2ndeqgOLD  31980  subtr2  32615  nn0prpwlem  32623  nn0prpw  32624  bj-axext3  33075  dfgcd3  33481  ftc1anclem6  33803  zindbi  38013  expdioph  38092  islssfg2  38143  eliunov2  38473  pm14.122b  39126