Theorem bibi1d 335

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  bibi12d  337  bibi1  343  biass  376  eubidvOLD  2620  eubidOLDOLD  2627  axext3  2756  axext3ALT  2757  axextmo  2759  bm1.1OLD  2760  eqeq1dALT  2781  pm13.183  3549  pm13.183OLD  3550  elabgt  3553  elrab3t  3571  mob  3600  reu6  3607  sbctt  3718  sbcabel  3734  isoeq2  6840  caovcang  7112  domunfican  8521  axacndlem4  9767  axacnd  9769  expeq0  13208  dfrtrclrec2  14204  relexpind  14211  sumodd  15518  prmdvdsexp  15831  isacs  16697  acsfn  16705  tsrlemax  17606  odeq  18353  isslw  18407  isabv  19211  t0sep  21536  xkopt  21867  kqt0lem  21948  r0sep  21960  nrmr0reg  21961  ismet  22536  isxmet  22537  stdbdxmet  22728  xrsxmet  23020  iccpnfcnv  23151  mdegle0  24274  isppw2  25293  tgjustf  25824  eleclclwwlkn  27474  eupth2lem1  27622  hvaddcan  28499  eigre  29266  xrge0iifcnv  30577  sgn0bi  31208  signswch  31238  bnj1468  31515  subtr2  32898  nn0prpwlem  32905  nn0prpw  32906  bj-axext3  33346  bj-bm1.3ii  33596  dfgcd3  33766  ftc1anclem6  34117  zindbi  38474  expdioph  38553  islssfg2  38604  eliunov2  38932  pm14.122b  39583  line2ylem  43491  line2xlem  43493