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 221	. 2 ⊢ ((𝜓 ↔ 𝜃) ↔ (𝜃 ↔ 𝜓))
4		bicom 221	. 2 ⊢ ((𝜒 ↔ 𝜃) ↔ (𝜃 ↔ 𝜒))
5	2, 3, 4	3bitr4g 313	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  345  bibi1  351  biass  385  axextg  2711  axextmo  2713  eqeq1dALT  2741  pm13.183  3590  elabgtOLD  3597  elrab3t  3616  mob  3647  reu6  3656  sbctt  3788  sbcabel  3807  isoeq2  7169  caovcang  7451  domunfican  9017  axacndlem4  10297  axacnd  10299  expeq0  13741  dfrtrclrec2  14697  relexpind  14703  sumodd  16025  prmdvdsexp  16348  isacs  17277  acsfn  17285  tsrlemax  18219  odeq  19073  isslw  19128  isabv  19994  t0sep  22383  xkopt  22714  kqt0lem  22795  r0sep  22807  nrmr0reg  22808  ismet  23384  isxmet  23385  stdbdxmet  23577  xrsxmet  23878  iccpnfcnv  24013  mdegle0  25147  isppw2  26169  tgjustf  26738  eleclclwwlkn  28341  eupth2lem1  28483  hvaddcan  29333  eigre  30098  opsbc2ie  30725  xrge0iifcnv  31785  sgn0bi  32414  signswch  32440  bnj1468  32726  subtr2  34431  nn0prpwlem  34438  nn0prpw  34439  bj-bm1.3ii  35162  dfgcd3  35422  ftc1anclem6  35782  zindbi  40684  expdioph  40761  islssfg2  40812  eliunov2  41176  pm14.122b  41930  elsetpreimafvbi  44731  line2ylem  45985  line2xlem  45987