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 ⊢ (𝜑 → ((𝜓 ↔ 𝜃) ↔ (𝜒 ↔ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  bibi12d  348  bibi1  354  biass  388  axextg  2737  axextmo  2739  eqeq1dALT  2766  pm13.183  3626  elrab3t  3650  mob  3681  reu6  3690  sbctt  3814  sbcabel  3832  isoeq2  7318  caovcang  7613  caofidlcan  7714  domunfican  9282  axacndlem4  10596  axacnd  10598  expeq0  14130  dfrtrclrec2  15097  relexpind  15103  sgn0bi  15142  sumodd  16447  prmdvdsexp  16775  isacs  17708  acsfn  17716  tsrlemax  18643  odeq  19621  isslw  19679  isabv  20895  t0sep  23462  xkopt  23793  kqt0lem  23874  r0sep  23886  nrmr0reg  23887  ismet  24461  isxmet  24462  stdbdxmet  24653  xrsxmet  24948  iccpnfcnv  25084  mdegle0  26215  isppw2  27257  tgjustf  28720  eleclclwwlkn  30405  eupth2lem1  30547  hvaddcan  31400  eigre  32165  opsbc2ie  32800  xrge0iifcnv  34301  signswch  34926  bnj1468  35212  axsepg3  35532  axsepg3ALT  35533  axsepg5  35535  subtr2  36804  nn0prpwlem  36811  nn0prpw  36812  bj-bm1.3ii  37678  dfgcd3  37946  ftc1anclem6  38327  zindbi  43653  expdioph  43730  islssfg2  43778  eliunov2  44385  pm14.122b  45113  omssaxinf2  45677  permaxrep  45695  permaxsep  45696  permaxinf2lem  45701  permac8prim  45703  elsetpreimafvbi  48117  line2ylem  49508  line2xlem  49510