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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  bibi12d  345  bibi1  351  biass  385  axextg  2704  axextmo  2706  eqeq1dALT  2734  pm13.183  3652  elabgtOLD  3659  elrab3t  3678  mob  3709  reu6  3718  sbctt  3849  sbcabel  3868  isoeq2  7299  caovcang  7591  domunfican  9303  axacndlem4  10587  axacnd  10589  expeq0  14040  dfrtrclrec2  14987  relexpind  14993  sumodd  16313  prmdvdsexp  16634  isacs  17577  acsfn  17585  tsrlemax  18521  odeq  19382  isslw  19440  isabv  20376  t0sep  22757  xkopt  23088  kqt0lem  23169  r0sep  23181  nrmr0reg  23182  ismet  23758  isxmet  23759  stdbdxmet  23953  xrsxmet  24254  iccpnfcnv  24389  mdegle0  25524  isppw2  26546  tgjustf  27589  eleclclwwlkn  29194  eupth2lem1  29336  hvaddcan  30186  eigre  30951  opsbc2ie  31579  xrge0iifcnv  32742  sgn0bi  33375  signswch  33401  bnj1468  33686  subtr2  35002  nn0prpwlem  35009  nn0prpw  35010  bj-bm1.3ii  35747  dfgcd3  36007  ftc1anclem6  36368  zindbi  41454  expdioph  41531  islssfg2  41582  eliunov2  42199  pm14.122b  42951  elsetpreimafvbi  45829  line2ylem  47083  line2xlem  47085