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  2708  axextmo  2710  eqeq1dALT  2738  pm13.183  3666  elabgtOLDOLD  3674  elrab3t  3694  mob  3726  reu6  3735  sbctt  3867  sbcabel  3887  isoeq2  7338  caovcang  7634  domunfican  9359  axacndlem4  10648  axacnd  10650  expeq0  14130  dfrtrclrec2  15094  relexpind  15100  sumodd  16422  prmdvdsexp  16749  isacs  17696  acsfn  17704  tsrlemax  18644  odeq  19583  isslw  19641  isabv  20829  t0sep  23348  xkopt  23679  kqt0lem  23760  r0sep  23772  nrmr0reg  23773  ismet  24349  isxmet  24350  stdbdxmet  24544  xrsxmet  24845  iccpnfcnv  24989  mdegle0  26131  isppw2  27173  tgjustf  28496  eleclclwwlkn  30105  eupth2lem1  30247  hvaddcan  31099  eigre  31864  opsbc2ie  32504  xrge0iifcnv  33894  sgn0bi  34529  signswch  34555  bnj1468  34839  axsepg2  35075  axsepg2ALT  35076  subtr2  36298  nn0prpwlem  36305  nn0prpw  36306  bj-bm1.3ii  37047  dfgcd3  37307  ftc1anclem6  37685  zindbi  42935  expdioph  43012  islssfg2  43060  eliunov2  43669  pm14.122b  44419  elsetpreimafvbi  47316  line2ylem  48601  line2xlem  48603