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  2706  axextmo  2708  eqeq1dALT  2736  pm13.183  3657  elabgtOLD  3664  elrab3t  3683  mob  3714  reu6  3723  sbctt  3854  sbcabel  3873  isoeq2  7315  caovcang  7608  domunfican  9320  axacndlem4  10605  axacnd  10607  expeq0  14058  dfrtrclrec2  15005  relexpind  15011  sumodd  16331  prmdvdsexp  16652  isacs  17595  acsfn  17603  tsrlemax  18539  odeq  19418  isslw  19476  isabv  20427  t0sep  22828  xkopt  23159  kqt0lem  23240  r0sep  23252  nrmr0reg  23253  ismet  23829  isxmet  23830  stdbdxmet  24024  xrsxmet  24325  iccpnfcnv  24460  mdegle0  25595  isppw2  26619  tgjustf  27755  eleclclwwlkn  29360  eupth2lem1  29502  hvaddcan  30354  eigre  31119  opsbc2ie  31747  xrge0iifcnv  32944  sgn0bi  33577  signswch  33603  bnj1468  33888  subtr2  35248  nn0prpwlem  35255  nn0prpw  35256  bj-bm1.3ii  35993  dfgcd3  36253  ftc1anclem6  36614  zindbi  41733  expdioph  41810  islssfg2  41861  eliunov2  42478  pm14.122b  43230  elsetpreimafvbi  46107  line2ylem  47485  line2xlem  47487