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  2737  axextmo  2739  eqeq1dALT  2766  pm13.183  3623  elrab3t  3647  mob  3678  reu6  3687  sbctt  3811  sbcabel  3829  isoeq2  7349  caovcang  7646  caofidlcan  7755  domunfican  9341  axacndlem4  10722  axacnd  10724  expeq0  14262  dfrtrclrec2  15240  relexpind  15246  sgn0bi  15285  sumodd  16587  prmdvdsexp  16920  isacs  17854  acsfn  17862  tsrlemax  18789  odeq  19794  isslw  19852  isabv  21098  t0sep  23672  xkopt  24004  kqt0lem  24085  r0sep  24097  nrmr0reg  24098  ismet  24672  isxmet  24673  stdbdxmet  24864  xrsxmet  25159  iccpnfcnv  25295  mdegle0  26425  isppw2  27472  tgjustf  28965  eleclclwwlkn  30697  eupth2lem1  30849  hvaddcan  31702  eigre  32467  opsbc2ie  33144  xrge0iifcnv  34635  signswch  35260  bnj1468  35546  reu6f  35779  axsepg3  35909  axsepg3ALT  35910  axsepg5  35912  subtr2  37281  nn0prpwlem  37288  nn0prpw  37289  bj-bm1.3ii  38170  dfgcd3  38437  ftc1anclem6  38808  zindbi  44146  expdioph  44223  islssfg2  44266  eliunov2  44871  pm14.122b  45598  omssaxinf2  46173  permaxrep  46191  permaxsep  46192  permaxinf2lem  46197  permac8prim  46199  elsetpreimafvbi  48678  line2ylem  50068  line2xlem  50070