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  3609  elrab3t  3634  mob  3664  reu6  3673  sbctt  3799  sbcabel  3817  isoeq2  7266  caovcang  7561  caofidlcan  7662  domunfican  9225  axacndlem4  10524  axacnd  10526  expeq0  14045  dfrtrclrec2  15011  relexpind  15017  sumodd  16348  prmdvdsexp  16676  isacs  17608  acsfn  17616  tsrlemax  18543  odeq  19516  isslw  19574  isabv  20779  t0sep  23299  xkopt  23630  kqt0lem  23711  r0sep  23723  nrmr0reg  23724  ismet  24298  isxmet  24299  stdbdxmet  24490  xrsxmet  24785  iccpnfcnv  24921  mdegle0  26052  isppw2  27092  tgjustf  28555  eleclclwwlkn  30161  eupth2lem1  30303  hvaddcan  31156  eigre  31921  opsbc2ie  32560  sgn0bi  32928  xrge0iifcnv  34093  signswch  34721  bnj1468  35004  axsepg2  35241  axsepg2ALT  35242  subtr2  36513  nn0prpwlem  36520  nn0prpw  36521  bj-bm1.3ii  37387  dfgcd3  37654  ftc1anclem6  38033  zindbi  43392  expdioph  43469  islssfg2  43517  eliunov2  44124  pm14.122b  44868  omssaxinf2  45433  permaxrep  45451  permaxsep  45452  permaxinf2lem  45457  permac8prim  45459  elsetpreimafvbi  47863  line2ylem  49239  line2xlem  49241