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  2703  axextmo  2705  eqeq1dALT  2732  pm13.183  3632  elrab3t  3658  mob  3688  reu6  3697  sbctt  3823  sbcabel  3841  isoeq2  7293  caovcang  7590  caofidlcan  7691  domunfican  9272  axacndlem4  10563  axacnd  10565  expeq0  14057  dfrtrclrec2  15024  relexpind  15030  sumodd  16358  prmdvdsexp  16685  isacs  17612  acsfn  17620  tsrlemax  18545  odeq  19480  isslw  19538  isabv  20720  t0sep  23211  xkopt  23542  kqt0lem  23623  r0sep  23635  nrmr0reg  23636  ismet  24211  isxmet  24212  stdbdxmet  24403  xrsxmet  24698  iccpnfcnv  24842  mdegle0  25982  isppw2  27025  tgjustf  28400  eleclclwwlkn  30005  eupth2lem1  30147  hvaddcan  30999  eigre  31764  opsbc2ie  32405  sgn0bi  32765  xrge0iifcnv  33923  signswch  34552  bnj1468  34836  axsepg2  35072  axsepg2ALT  35073  subtr2  36303  nn0prpwlem  36310  nn0prpw  36311  bj-bm1.3ii  37052  dfgcd3  37312  ftc1anclem6  37692  zindbi  42935  expdioph  43012  islssfg2  43060  eliunov2  43668  pm14.122b  44412  omssaxinf2  44978  permaxrep  44996  permaxsep  44997  permaxinf2lem  45002  permac8prim  45004  elsetpreimafvbi  47392  line2ylem  48740  line2xlem  48742