Theorem bibi1d 344

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bibi12d  346  bibi1  352  biass  386  axextg  2712  axextmo  2714  eqeq1dALT  2742  pm13.183  3598  elabgtOLD  3605  elrab3t  3624  mob  3653  reu6  3662  sbctt  3793  sbcabel  3812  isoeq2  7198  caovcang  7482  domunfican  9096  axacndlem4  10375  axacnd  10377  expeq0  13822  dfrtrclrec2  14778  relexpind  14784  sumodd  16106  prmdvdsexp  16429  isacs  17369  acsfn  17377  tsrlemax  18313  odeq  19167  isslw  19222  isabv  20088  t0sep  22484  xkopt  22815  kqt0lem  22896  r0sep  22908  nrmr0reg  22909  ismet  23485  isxmet  23486  stdbdxmet  23680  xrsxmet  23981  iccpnfcnv  24116  mdegle0  25251  isppw2  26273  tgjustf  26843  eleclclwwlkn  28449  eupth2lem1  28591  hvaddcan  29441  eigre  30206  opsbc2ie  30833  xrge0iifcnv  31892  sgn0bi  32523  signswch  32549  bnj1468  32835  subtr2  34513  nn0prpwlem  34520  nn0prpw  34521  bj-bm1.3ii  35244  dfgcd3  35504  ftc1anclem6  35864  zindbi  40775  expdioph  40852  islssfg2  40903  eliunov2  41294  pm14.122b  42048  elsetpreimafvbi  44854  line2ylem  46108  line2xlem  46110