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  2739  pm13.183  3620  elrab3t  3645  mob  3675  reu6  3684  sbctt  3810  sbcabel  3828  isoeq2  7264  caovcang  7559  caofidlcan  7660  domunfican  9222  axacndlem4  10521  axacnd  10523  expeq0  14015  dfrtrclrec2  14981  relexpind  14987  sumodd  16315  prmdvdsexp  16642  isacs  17574  acsfn  17582  tsrlemax  18509  odeq  19479  isslw  19537  isabv  20744  t0sep  23268  xkopt  23599  kqt0lem  23680  r0sep  23692  nrmr0reg  23693  ismet  24267  isxmet  24268  stdbdxmet  24459  xrsxmet  24754  iccpnfcnv  24898  mdegle0  26038  isppw2  27081  tgjustf  28545  eleclclwwlkn  30151  eupth2lem1  30293  hvaddcan  31145  eigre  31910  opsbc2ie  32550  sgn0bi  32921  xrge0iifcnv  34090  signswch  34718  bnj1468  35002  axsepg2  35238  axsepg2ALT  35239  subtr2  36509  nn0prpwlem  36516  nn0prpw  36517  bj-bm1.3ii  37265  dfgcd3  37525  ftc1anclem6  37895  zindbi  43184  expdioph  43261  islssfg2  43309  eliunov2  43916  pm14.122b  44660  omssaxinf2  45225  permaxrep  45243  permaxsep  45244  permaxinf2lem  45249  permac8prim  45251  elsetpreimafvbi  47633  line2ylem  48993  line2xlem  48995