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  2711  axextmo  2713  eqeq1dALT  2740  pm13.183  3622  elrab3t  3647  mob  3677  reu6  3686  sbctt  3812  sbcabel  3830  isoeq2  7274  caovcang  7569  caofidlcan  7670  domunfican  9234  axacndlem4  10533  axacnd  10535  expeq0  14027  dfrtrclrec2  14993  relexpind  14999  sumodd  16327  prmdvdsexp  16654  isacs  17586  acsfn  17594  tsrlemax  18521  odeq  19491  isslw  19549  isabv  20756  t0sep  23280  xkopt  23611  kqt0lem  23692  r0sep  23704  nrmr0reg  23705  ismet  24279  isxmet  24280  stdbdxmet  24471  xrsxmet  24766  iccpnfcnv  24910  mdegle0  26050  isppw2  27093  tgjustf  28557  eleclclwwlkn  30163  eupth2lem1  30305  hvaddcan  31157  eigre  31922  opsbc2ie  32561  sgn0bi  32931  xrge0iifcnv  34110  signswch  34738  bnj1468  35021  axsepg2  35257  axsepg2ALT  35258  subtr2  36528  nn0prpwlem  36535  nn0prpw  36536  bj-bm1.3ii  37306  dfgcd3  37573  ftc1anclem6  37943  zindbi  43297  expdioph  43374  islssfg2  43422  eliunov2  44029  pm14.122b  44773  omssaxinf2  45338  permaxrep  45356  permaxsep  45357  permaxinf2lem  45362  permac8prim  45364  elsetpreimafvbi  47745  line2ylem  49105  line2xlem  49107