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  2705  axextmo  2707  eqeq1dALT  2734  pm13.183  3616  elrab3t  3641  mob  3671  reu6  3680  sbctt  3806  sbcabel  3824  isoeq2  7258  caovcang  7553  caofidlcan  7654  domunfican  9212  axacndlem4  10507  axacnd  10509  expeq0  14005  dfrtrclrec2  14971  relexpind  14977  sumodd  16305  prmdvdsexp  16632  isacs  17563  acsfn  17571  tsrlemax  18498  odeq  19468  isslw  19526  isabv  20732  t0sep  23245  xkopt  23576  kqt0lem  23657  r0sep  23669  nrmr0reg  23670  ismet  24244  isxmet  24245  stdbdxmet  24436  xrsxmet  24731  iccpnfcnv  24875  mdegle0  26015  isppw2  27058  tgjustf  28457  eleclclwwlkn  30063  eupth2lem1  30205  hvaddcan  31057  eigre  31822  opsbc2ie  32462  sgn0bi  32830  xrge0iifcnv  33953  signswch  34581  bnj1468  34865  axsepg2  35101  axsepg2ALT  35102  subtr2  36366  nn0prpwlem  36373  nn0prpw  36374  bj-bm1.3ii  37115  dfgcd3  37375  ftc1anclem6  37744  zindbi  43044  expdioph  43121  islssfg2  43169  eliunov2  43777  pm14.122b  44521  omssaxinf2  45086  permaxrep  45104  permaxsep  45105  permaxinf2lem  45110  permac8prim  45112  elsetpreimafvbi  47496  line2ylem  48857  line2xlem  48859