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  2710  axextmo  2712  eqeq1dALT  2740  pm13.183  3666  elrab3t  3691  mob  3723  reu6  3732  sbctt  3860  sbcabel  3878  isoeq2  7338  caovcang  7634  caofidlcan  7735  domunfican  9361  axacndlem4  10650  axacnd  10652  expeq0  14133  dfrtrclrec2  15097  relexpind  15103  sumodd  16425  prmdvdsexp  16752  isacs  17694  acsfn  17702  tsrlemax  18631  odeq  19568  isslw  19626  isabv  20812  t0sep  23332  xkopt  23663  kqt0lem  23744  r0sep  23756  nrmr0reg  23757  ismet  24333  isxmet  24334  stdbdxmet  24528  xrsxmet  24831  iccpnfcnv  24975  mdegle0  26116  isppw2  27158  tgjustf  28481  eleclclwwlkn  30095  eupth2lem1  30237  hvaddcan  31089  eigre  31854  opsbc2ie  32495  xrge0iifcnv  33932  sgn0bi  34550  signswch  34576  bnj1468  34860  axsepg2  35096  axsepg2ALT  35097  subtr2  36316  nn0prpwlem  36323  nn0prpw  36324  bj-bm1.3ii  37065  dfgcd3  37325  ftc1anclem6  37705  zindbi  42958  expdioph  43035  islssfg2  43083  eliunov2  43692  pm14.122b  44442  omssaxinf2  45005  elsetpreimafvbi  47378  line2ylem  48672  line2xlem  48674