Theorem bibi1d 344

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  bibi12d  346  bibi1  352  biass  385  axextg  2714  axextmo  2716  eqeq1dALT  2743  pm13.183  3611  elrab3t  3635  mob  3665  reu6  3674  sbctt  3799  sbcabel  3817  isoeq2  7269  caovcang  7564  caofidlcan  7665  domunfican  9229  axacndlem4  10531  axacnd  10533  expeq0  14052  dfrtrclrec2  15018  relexpind  15024  sumodd  16355  prmdvdsexp  16683  isacs  17615  acsfn  17623  tsrlemax  18550  odeq  19523  isslw  19581  isabv  20790  t0sep  23314  xkopt  23645  kqt0lem  23726  r0sep  23738  nrmr0reg  23739  ismet  24313  isxmet  24314  stdbdxmet  24505  xrsxmet  24800  iccpnfcnv  24936  mdegle0  26067  isppw2  27103  tgjustf  28566  eleclclwwlkn  30171  eupth2lem1  30313  hvaddcan  31166  eigre  31931  opsbc2ie  32570  sgn0bi  32939  xrge0iifcnv  34124  signswch  34752  bnj1468  35035  axsepg3  35329  axsepg3ALT  35330  axsepg5  35332  subtr2  36550  nn0prpwlem  36557  nn0prpw  36558  bj-bm1.3ii  37424  dfgcd3  37691  ftc1anclem6  38072  zindbi  43398  expdioph  43475  islssfg2  43523  eliunov2  44130  pm14.122b  44874  omssaxinf2  45439  permaxrep  45457  permaxsep  45458  permaxinf2lem  45463  permac8prim  45465  elsetpreimafvbi  47873  line2ylem  49249  line2xlem  49251