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

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  bibi12d  348  bibi1  354  biass  388  axextg  2793  axextmo  2795  eqeq1dALT  2822  pm13.183  3657  pm13.183OLD  3658  elabgt  3661  elrab3t  3677  mob  3706  reu6  3715  sbctt  3842  sbcabel  3859  isoeq2  7063  caovcang  7341  domunfican  8783  axacndlem4  10024  axacnd  10026  expeq0  13451  dfrtrclrec2  14408  relexpind  14415  sumodd  15731  prmdvdsexp  16051  isacs  16914  acsfn  16922  tsrlemax  17822  odeq  18670  isslw  18725  isabv  19582  t0sep  21924  xkopt  22255  kqt0lem  22336  r0sep  22348  nrmr0reg  22349  ismet  22925  isxmet  22926  stdbdxmet  23117  xrsxmet  23409  iccpnfcnv  23540  mdegle0  24663  isppw2  25684  tgjustf  26251  eleclclwwlkn  27847  eupth2lem1  27989  hvaddcan  28839  eigre  29604  opsbc2ie  30231  xrge0iifcnv  31169  sgn0bi  31798  signswch  31824  bnj1468  32111  subtr2  33656  nn0prpwlem  33663  nn0prpw  33664  bj-bm1.3ii  34349  dfgcd3  34597  ftc1anclem6  34964  zindbi  39533  expdioph  39610  islssfg2  39661  eliunov2  40014  pm14.122b  40745  elsetpreimafvbi  43541  line2ylem  44728  line2xlem  44730