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  2739  axextmo  2741  eqeq1dALT  2768  pm13.183  3628  elrab3t  3652  mob  3683  reu6  3692  sbctt  3816  sbcabel  3834  isoeq2  7306  caovcang  7601  caofidlcan  7702  domunfican  9269  axacndlem4  10583  axacnd  10585  expeq0  14119  dfrtrclrec2  15085  relexpind  15091  sgn0bi  15130  sumodd  16436  prmdvdsexp  16764  isacs  17697  acsfn  17705  tsrlemax  18632  odeq  19611  isslw  19669  isabv  20883  t0sep  23442  xkopt  23773  kqt0lem  23854  r0sep  23866  nrmr0reg  23867  ismet  24441  isxmet  24442  stdbdxmet  24633  xrsxmet  24928  iccpnfcnv  25064  mdegle0  26195  isppw2  27237  tgjustf  28700  eleclclwwlkn  30336  eupth2lem1  30478  hvaddcan  31331  eigre  32096  opsbc2ie  32732  xrge0iifcnv  34240  signswch  34865  bnj1468  35151  axsepg3  35449  axsepg3ALT  35450  axsepg5  35452  subtr2  36688  nn0prpwlem  36695  nn0prpw  36696  bj-bm1.3ii  37561  dfgcd3  37828  ftc1anclem6  38209  zindbi  43535  expdioph  43612  islssfg2  43660  eliunov2  44267  pm14.122b  44997  omssaxinf2  45562  permaxrep  45580  permaxsep  45581  permaxinf2lem  45586  permac8prim  45588  elsetpreimafvbi  47995  line2ylem  49382  line2xlem  49384