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  2713  axextmo  2715  eqeq1dALT  2743  pm13.183  3679  elabgtOLDOLD  3687  elrab3t  3707  mob  3739  reu6  3748  sbctt  3880  sbcabel  3900  isoeq2  7354  caovcang  7651  domunfican  9389  axacndlem4  10679  axacnd  10681  expeq0  14143  dfrtrclrec2  15107  relexpind  15113  sumodd  16436  prmdvdsexp  16762  isacs  17709  acsfn  17717  tsrlemax  18656  odeq  19592  isslw  19650  isabv  20834  t0sep  23353  xkopt  23684  kqt0lem  23765  r0sep  23777  nrmr0reg  23778  ismet  24354  isxmet  24355  stdbdxmet  24549  xrsxmet  24850  iccpnfcnv  24994  mdegle0  26136  isppw2  27176  tgjustf  28499  eleclclwwlkn  30108  eupth2lem1  30250  hvaddcan  31102  eigre  31867  opsbc2ie  32504  xrge0iifcnv  33879  sgn0bi  34512  signswch  34538  bnj1468  34822  axsepg2  35058  axsepg2ALT  35059  subtr2  36281  nn0prpwlem  36288  nn0prpw  36289  bj-bm1.3ii  37030  dfgcd3  37290  ftc1anclem6  37658  zindbi  42903  expdioph  42980  islssfg2  43028  eliunov2  43641  pm14.122b  44392  elsetpreimafvbi  47265  line2ylem  48485  line2xlem  48487