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  2709  axextmo  2711  eqeq1dALT  2738  pm13.183  3645  elrab3t  3670  mob  3700  reu6  3709  sbctt  3835  sbcabel  3853  isoeq2  7311  caovcang  7608  caofidlcan  7709  domunfican  9333  axacndlem4  10624  axacnd  10626  expeq0  14110  dfrtrclrec2  15077  relexpind  15083  sumodd  16407  prmdvdsexp  16734  isacs  17663  acsfn  17671  tsrlemax  18596  odeq  19531  isslw  19589  isabv  20771  t0sep  23262  xkopt  23593  kqt0lem  23674  r0sep  23686  nrmr0reg  23687  ismet  24262  isxmet  24263  stdbdxmet  24454  xrsxmet  24749  iccpnfcnv  24893  mdegle0  26034  isppw2  27077  tgjustf  28452  eleclclwwlkn  30057  eupth2lem1  30199  hvaddcan  31051  eigre  31816  opsbc2ie  32457  sgn0bi  32819  xrge0iifcnv  33964  signswch  34593  bnj1468  34877  axsepg2  35113  axsepg2ALT  35114  subtr2  36333  nn0prpwlem  36340  nn0prpw  36341  bj-bm1.3ii  37082  dfgcd3  37342  ftc1anclem6  37722  zindbi  42970  expdioph  43047  islssfg2  43095  eliunov2  43703  pm14.122b  44447  omssaxinf2  45013  permaxrep  45031  permaxsep  45032  permaxinf2lem  45037  elsetpreimafvbi  47405  line2ylem  48731  line2xlem  48733