Theorem bibi1d 346

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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bibi12d  348  bibi1  354  biass  388  axextg  2797  axextmo  2799  eqeq1dALT  2826  pm13.183  3661  pm13.183OLD  3662  elabgt  3665  elrab3t  3681  mob  3710  reu6  3719  sbctt  3846  sbcabel  3863  isoeq2  7073  caovcang  7351  domunfican  8793  axacndlem4  10034  axacnd  10036  expeq0  13462  dfrtrclrec2  14418  relexpind  14425  sumodd  15741  prmdvdsexp  16061  isacs  16924  acsfn  16932  tsrlemax  17832  odeq  18680  isslw  18735  isabv  19592  t0sep  21934  xkopt  22265  kqt0lem  22346  r0sep  22358  nrmr0reg  22359  ismet  22935  isxmet  22936  stdbdxmet  23127  xrsxmet  23419  iccpnfcnv  23550  mdegle0  24673  isppw2  25694  tgjustf  26261  eleclclwwlkn  27857  eupth2lem1  27999  hvaddcan  28849  eigre  29614  opsbc2ie  30241  xrge0iifcnv  31178  sgn0bi  31807  signswch  31833  bnj1468  32120  subtr2  33665  nn0prpwlem  33672  nn0prpw  33673  bj-bm1.3ii  34359  dfgcd3  34607  ftc1anclem6  34974  zindbi  39550  expdioph  39627  islssfg2  39678  eliunov2  40031  pm14.122b  40762  elsetpreimafvbi  43558  line2ylem  44745  line2xlem  44747