Theorem bibi1d 347

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 346	. 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  349  bibi1  355  biass  389  axextg  2712  axextmo  2714  eqeq1dALT  2741  pm13.183  3564  elabgt  3567  elrab3t  3587  mob  3616  reu6  3625  sbctt  3752  sbcabel  3769  csb0  4296  isoeq2  7084  caovcang  7365  domunfican  8865  axacndlem4  10110  axacnd  10112  expeq0  13551  dfrtrclrec2  14507  relexpind  14513  sumodd  15833  prmdvdsexp  16156  isacs  17025  acsfn  17033  tsrlemax  17946  odeq  18796  isslw  18851  isabv  19709  t0sep  22075  xkopt  22406  kqt0lem  22487  r0sep  22499  nrmr0reg  22500  ismet  23076  isxmet  23077  stdbdxmet  23268  xrsxmet  23561  iccpnfcnv  23696  mdegle0  24830  isppw2  25852  tgjustf  26419  eleclclwwlkn  28013  eupth2lem1  28155  hvaddcan  29005  eigre  29770  opsbc2ie  30398  xrge0iifcnv  31455  sgn0bi  32084  signswch  32110  bnj1468  32397  subtr2  34142  nn0prpwlem  34149  nn0prpw  34150  bj-bm1.3ii  34858  dfgcd3  35115  ftc1anclem6  35478  zindbi  40340  expdioph  40417  islssfg2  40468  eliunov2  40833  pm14.122b  41579  elsetpreimafvbi  44377  line2ylem  45631  line2xlem  45633