Theorem bibi1d 346

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  bibi12d  348  bibi1  354  biass  388  axextg  2735  axextmo  2737  eqeq1dALT  2764  pm13.183  3620  elrab3t  3644  mob  3675  reu6  3684  sbctt  3808  sbcabel  3825  isoeq2  7318  caovcang  7614  caofidlcan  7720  domunfican  9297  axacndlem4  10676  axacnd  10678  expeq0  14215  dfrtrclrec2  15191  relexpind  15197  sgn0bi  15236  sumodd  16538  prmdvdsexp  16871  isacs  17805  acsfn  17813  tsrlemax  18740  odeq  19744  isslw  19802  isabv  21048  t0sep  23622  xkopt  23954  kqt0lem  24035  r0sep  24047  nrmr0reg  24048  ismet  24622  isxmet  24623  stdbdxmet  24814  xrsxmet  25109  iccpnfcnv  25245  mdegle0  26375  isppw2  27424  tgjustf  28917  eleclclwwlkn  30649  eupth2lem1  30801  hvaddcan  31654  eigre  32419  opsbc2ie  33054  xrge0iifcnv  34547  signswch  35173  bnj1468  35459  axsepg3  35782  axsepg3ALT  35783  axsepg5  35785  subtr2  37073  nn0prpwlem  37080  nn0prpw  37081  bj-bm1.3ii  37947  dfgcd3  38213  ftc1anclem6  38584  zindbi  43906  expdioph  43983  islssfg2  44031  eliunov2  44638  pm14.122b  45366  omssaxinf2  45930  permaxrep  45948  permaxsep  45949  permaxinf2lem  45954  permac8prim  45956  elsetpreimafvbi  48417  line2ylem  49807  line2xlem  49809