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  2705  axextmo  2707  eqeq1dALT  2734  pm13.183  3621  elrab3t  3646  mob  3676  reu6  3685  sbctt  3811  sbcabel  3829  isoeq2  7252  caovcang  7547  caofidlcan  7648  domunfican  9206  axacndlem4  10501  axacnd  10503  expeq0  13999  dfrtrclrec2  14965  relexpind  14971  sumodd  16299  prmdvdsexp  16626  isacs  17557  acsfn  17565  tsrlemax  18492  odeq  19463  isslw  19521  isabv  20727  t0sep  23240  xkopt  23571  kqt0lem  23652  r0sep  23664  nrmr0reg  23665  ismet  24239  isxmet  24240  stdbdxmet  24431  xrsxmet  24726  iccpnfcnv  24870  mdegle0  26010  isppw2  27053  tgjustf  28452  eleclclwwlkn  30054  eupth2lem1  30196  hvaddcan  31048  eigre  31813  opsbc2ie  32453  sgn0bi  32821  xrge0iifcnv  33944  signswch  34572  bnj1468  34856  axsepg2  35092  axsepg2ALT  35093  subtr2  36355  nn0prpwlem  36362  nn0prpw  36363  bj-bm1.3ii  37104  dfgcd3  37364  ftc1anclem6  37744  zindbi  42985  expdioph  43062  islssfg2  43110  eliunov2  43718  pm14.122b  44462  omssaxinf2  45027  permaxrep  45045  permaxsep  45046  permaxinf2lem  45051  permac8prim  45053  elsetpreimafvbi  47428  line2ylem  48789  line2xlem  48791