Theorem bibi1d 347

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bibi12d  349  bibi1  355  biass  389  axextg  2772  axextmo  2774  eqeq1dALT  2801  pm13.183  3606  elabgt  3609  elrab3t  3627  mob  3656  reu6  3665  sbctt  3790  sbcabel  3807  csb0  4314  isoeq2  7050  caovcang  7329  domunfican  8775  axacndlem4  10021  axacnd  10023  expeq0  13455  dfrtrclrec2  14409  relexpind  14415  sumodd  15729  prmdvdsexp  16049  isacs  16914  acsfn  16922  tsrlemax  17822  odeq  18670  isslw  18725  isabv  19583  t0sep  21929  xkopt  22260  kqt0lem  22341  r0sep  22353  nrmr0reg  22354  ismet  22930  isxmet  22931  stdbdxmet  23122  xrsxmet  23414  iccpnfcnv  23549  mdegle0  24678  isppw2  25700  tgjustf  26267  eleclclwwlkn  27861  eupth2lem1  28003  hvaddcan  28853  eigre  29618  opsbc2ie  30246  xrge0iifcnv  31286  sgn0bi  31915  signswch  31941  bnj1468  32228  subtr2  33776  nn0prpwlem  33783  nn0prpw  33784  bj-bm1.3ii  34481  dfgcd3  34738  ftc1anclem6  35135  zindbi  39887  expdioph  39964  islssfg2  40015  eliunov2  40380  pm14.122b  41127  elsetpreimafvbi  43908  line2ylem  45165  line2xlem  45167