Theorem 3bitr2i 288

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2i.1	⊢ (𝜑 ↔ 𝜓)
3bitr2i.2	⊢ (𝜒 ↔ 𝜓)
3bitr2i.3	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
3bitr2i	⊢ (𝜑 ↔ 𝜃)

Proof of Theorem 3bitr2i

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
2		3bitr2i.2	. . 3 ⊢ (𝜒 ↔ 𝜓)
3	1, 2	bitr4i 267	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitri 264	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 196

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 197

This theorem is referenced by:  con2bi  343  an13  840  xorneg2  1474  2eu4  2556  2eu5  2557  exists1  2561  euxfr  3392  euind  3393  rmo4  3399  2reu5lem3  3415  rmo3  3528  difin  3861  reusv2lem4  4872  rabxp  5154  elvvv  5178  eliunxp  5259  imadisj  5484  intirr  5514  resco  5639  funcnv3  5959  fncnv  5962  fun11  5963  fununi  5964  mptfnf  6015  f1mpt  6518  mpt2mptx  6751  uniuni  6971  frxp  7287  oeeu  7683  ixp0x  7936  mapsnen  8035  xpcomco  8050  1sdom  8163  dffi3  8337  wemapsolem  8455  cardval3  8778  kmlem4  8975  kmlem12  8983  kmlem14  8985  kmlem15  8986  kmlem16  8987  fpwwe2  9465  axgroth4  9654  ltexprlem4  9861  bitsmod  15158  pythagtrip  15539  pgpfac1  18479  pgpfac  18483  isassa  19315  basdif0  20757  ntreq0  20881  tgcmp  21204  tx1cn  21412  rnelfmlem  21756  phtpcer  22794  phtpcerOLD  22795  iscvsp  22928  caucfil  23081  minveclem1  23195  ovoliunlem1  23270  mdegleb  23824  istrkg2ld  25359  numedglnl  26039  usgr2pth0  26661  adjbd1o  28944  nmo  29325  rmo3f  29335  rmo4fOLD  29336  difrab2  29339  mpt2mptxf  29477  isros  30231  1stmbfm  30322  bnj976  30848  bnj1143  30861  bnj1533  30922  bnj864  30992  bnj983  31021  bnj1174  31071  bnj1175  31072  bnj1280  31088  cvmlift2lem12  31296  axacprim  31584  dmscut  31918  dfrecs2  32057  andnand1  32398  bj-dfssb2  32640  bj-denotes  32858  bj-snglc  32957  bj-disj2r  33013  bj-dfmpt2a  33071  bj-mpt2mptALT  33072  mptsnunlem  33185  wl-cases2-dnf  33295  itg2addnc  33464  asindmre  33495  brres2  34035  isopos  34467  dihglblem6  36629  dihglb2  36631  fgraphopab  37788  ifpid2g  37838  ifpim23g  37840  rp-fakeanorass  37858  elmapintrab  37882  relintabex  37887  relnonrel  37893  undmrnresiss  37910  elintima  37945  relexp0eq  37993  iunrelexp0  37994  dffrege115  38272  frege131  38288  frege133  38290  ntrneikb  38392  onfrALTlem5  38757  ndisj2  39218  ndmaovcom  41285  eliunxp2  42112  mpt2mptx2  42113  alimp-no-surprise  42527  alsi-no-surprise  42542