Theorem bibi1d 346

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi12d  348  bibi1  354  biass  388  axextg  2734  axextmo  2736  eqeq1dALT  2763  pm13.183  3619  elrab3t  3643  mob  3674  reu6  3683  sbctt  3807  sbcabel  3824  isoeq2  7326  caovcang  7622  caofidlcan  7731  domunfican  9316  axacndlem4  10698  axacnd  10700  expeq0  14238  dfrtrclrec2  15216  relexpind  15222  sgn0bi  15261  sumodd  16563  prmdvdsexp  16896  isacs  17830  acsfn  17838  tsrlemax  18765  odeq  19769  isslw  19827  isabv  21073  t0sep  23647  xkopt  23979  kqt0lem  24060  r0sep  24072  nrmr0reg  24073  ismet  24647  isxmet  24648  stdbdxmet  24839  xrsxmet  25134  iccpnfcnv  25270  mdegle0  26400  isppw2  27447  tgjustf  28940  eleclclwwlkn  30672  eupth2lem1  30824  hvaddcan  31677  eigre  32442  opsbc2ie  33119  xrge0iifcnv  34611  signswch  35236  bnj1468  35522  reu6f  35755  axsepg3  35865  axsepg3ALT  35866  axsepg5  35868  subtr2  37195  nn0prpwlem  37202  nn0prpw  37203  bj-bm1.3ii  38071  dfgcd3  38338  ftc1anclem6  38709  zindbi  44046  expdioph  44123  islssfg2  44166  eliunov2  44772  pm14.122b  45500  omssaxinf2  46071  permaxrep  46089  permaxsep  46090  permaxinf2lem  46095  permac8prim  46097  elsetpreimafvbi  48566  line2ylem  49956  line2xlem  49958