Theorem bibi1d 332

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

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  bibi12d  334  bibi1  340  biass  373  eubid  2476  axext3  2592  axext3ALT  2593  bm1.1  2595  eqeq1dALT  2613  pm13.183  3313  elabgt  3316  elrab3t  3330  mob  3355  reu6  3362  sbctt  3467  sbcabel  3483  isoeq2  6468  caovcang  6733  domunfican  8118  axacndlem4  9311  axacnd  9313  expeq0  12752  dfrtrclrec2  13645  relexpind  13652  sumodd  14949  prmdvdsexp  15265  isacs  16135  acsfn  16143  tsrlemax  17043  odeq  17792  isslw  17846  isabv  18642  t0sep  20938  xkopt  21268  kqt0lem  21349  r0sep  21361  nrmr0reg  21362  ismet  21938  isxmet  21939  stdbdxmet  22130  xrsxmet  22420  iccpnfcnv  22551  mdegle0  23641  isppw2  24641  cusgrauvtxb  26024  eleclclwwlkn  26360  eupath2lem1  26504  hvaddcan  27311  eigre  28078  xrge0iifcnv  29307  sgn0bi  29936  signswch  29964  bnj1468  30170  br1steqg  30919  br2ndeqg  30920  subtr2  31479  nn0prpwlem  31487  nn0prpw  31488  bj-axext3  31957  ftc1anclem6  32660  zindbi  36529  expdioph  36608  islssfg2  36659  eliunov2  36990  pm14.122b  37646  eleclclwwlksn  41260  eupth2lem1  41386