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  2704  axextmo  2706  eqeq1dALT  2734  pm13.183  3652  elabgtOLD  3659  elrab3t  3678  mob  3709  reu6  3718  sbctt  3849  sbcabel  3868  isoeq2  7299  caovcang  7591  domunfican  9303  axacndlem4  10587  axacnd  10589  expeq0  14040  dfrtrclrec2  14987  relexpind  14993  sumodd  16313  prmdvdsexp  16634  isacs  17577  acsfn  17585  tsrlemax  18521  odeq  19382  isslw  19440  isabv  20376  t0sep  22757  xkopt  23088  kqt0lem  23169  r0sep  23181  nrmr0reg  23182  ismet  23758  isxmet  23759  stdbdxmet  23953  xrsxmet  24254  iccpnfcnv  24389  mdegle0  25524  isppw2  26546  tgjustf  27589  eleclclwwlkn  29194  eupth2lem1  29336  hvaddcan  30186  eigre  30951  opsbc2ie  31579  xrge0iifcnv  32744  sgn0bi  33377  signswch  33403  bnj1468  33688  subtr2  35004  nn0prpwlem  35011  nn0prpw  35012  bj-bm1.3ii  35749  dfgcd3  36009  ftc1anclem6  36370  zindbi  41456  expdioph  41533  islssfg2  41584  eliunov2  42201  pm14.122b  42953  elsetpreimafvbi  45831  line2ylem  47085  line2xlem  47087