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  2703  axextmo  2705  eqeq1dALT  2732  pm13.183  3623  elrab3t  3649  mob  3679  reu6  3688  sbctt  3814  sbcabel  3832  isoeq2  7259  caovcang  7554  caofidlcan  7655  domunfican  9230  axacndlem4  10523  axacnd  10525  expeq0  14017  dfrtrclrec2  14983  relexpind  14989  sumodd  16317  prmdvdsexp  16644  isacs  17575  acsfn  17583  tsrlemax  18510  odeq  19447  isslw  19505  isabv  20714  t0sep  23227  xkopt  23558  kqt0lem  23639  r0sep  23651  nrmr0reg  23652  ismet  24227  isxmet  24228  stdbdxmet  24419  xrsxmet  24714  iccpnfcnv  24858  mdegle0  25998  isppw2  27041  tgjustf  28436  eleclclwwlkn  30038  eupth2lem1  30180  hvaddcan  31032  eigre  31797  opsbc2ie  32438  sgn0bi  32798  xrge0iifcnv  33902  signswch  34531  bnj1468  34815  axsepg2  35051  axsepg2ALT  35052  subtr2  36291  nn0prpwlem  36298  nn0prpw  36299  bj-bm1.3ii  37040  dfgcd3  37300  ftc1anclem6  37680  zindbi  42922  expdioph  42999  islssfg2  43047  eliunov2  43655  pm14.122b  44399  omssaxinf2  44965  permaxrep  44983  permaxsep  44984  permaxinf2lem  44989  permac8prim  44991  elsetpreimafvbi  47379  line2ylem  48740  line2xlem  48742