Theorem 3bitr2i 302

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 281	. 2 ⊢ (𝜑 ↔ 𝜒)
4		3bitr2i.3	. 2 ⊢ (𝜒 ↔ 𝜃)
5	3, 4	bitri 278	1 ⊢ (𝜑 ↔ 𝜃)

Syntax hints:   ↔ wb 209

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 210

This theorem is referenced by:  con2bi  357  xorneg2  1514  sbrimvlem  2099  dfsb7OLD  2283  2eu4  2676  2eu5  2677  2eu5OLD  2678  euxfrw  3638  euxfr  3640  euind  3641  rmo4  3647  rmo3f  3651  2reu5lem3  3674  rmo3  3798  difin  4169  indifdi  4191  ab0orv  4279  axsepgfromrep  5172  reusv2lem4  5275  rabxp  5575  elvvv  5602  eliunxp  5684  elidinxp  5889  imadisj  5926  idrefALT  5951  intirr  5956  resco  6086  funcnv3  6411  fncnv  6414  fun11  6415  fununi  6416  mptfnf  6472  f1mpt  7018  mpomptx  7266  uniuni  7490  frxp  7832  oeeu  8246  ixp0x  8522  xpcomco  8642  1sdom  8773  dffi3  8942  wemapsolem  9061  cardval3  9428  kmlem4  9627  kmlem12  9635  kmlem14  9637  kmlem15  9638  kmlem16  9639  fpwwe2  10117  axgroth4  10306  ltexprlem4  10513  bitsmod  15849  pythagtrip  16241  isstruct  16569  pgpfac1  19285  pgpfac  19289  isassa  20636  basdif0  21668  ntreq0  21792  tgcmp  22116  tx1cn  22324  rnelfmlem  22667  phtpcer  23711  iscvsp  23844  caucfil  23998  minveclem1  24139  ovoliunlem1  24217  mdegleb  24779  istrkg2ld  26368  numedglnl  27051  usgr2pth0  27668  adjbd1o  29982  nelbOLD  30353  nmo  30375  dmrab  30381  difrab2  30382  mpomptxf  30554  ccfldextdgrr  31277  isros  31669  1stmbfm  31760  bnj976  32291  bnj1143  32304  bnj1533  32366  bnj864  32436  bnj983  32465  bnj1174  32517  bnj1175  32518  bnj1280  32534  cvmlift2lem12  32806  axacprim  33178  xpord2pred  33361  xpord2ind  33363  eqscut2  33597  dmscut  33602  made0  33650  dfrecs2  33837  andnand1  34175  bj-snglc  34722  bj-disj2r  34781  bj-dfmpoa  34849  bj-mpomptALT  34850  mptsnunlem  35071  wl-df3xor2  35202  wl-df4-3mintru2  35220  wl-cases2-dnf  35233  wl-euae  35238  wl-dfralv  35322  itg2addnc  35427  asindmre  35456  brres2  36005  brxrn2  36103  dfxrn2  36104  inxpxrn  36119  refsymrel2  36279  refsymrel3  36280  dfeqvrel2  36301  dfeqvrel3  36302  isopos  36792  dihglblem6  38952  dihglb2  38954  fgraphopab  40573  ifpid2g  40620  ifpim23g  40622  rp-fakeanorass  40640  en2pr  40665  elmapintrab  40695  relnonrel  40706  undmrnresiss  40723  elintima  40773  relexp0eq  40821  iunrelexp0  40822  dffrege115  41098  frege131  41114  frege133  41116  ntrneikb  41216  onfrALTlem5  41667  onfrALTlem5VD  42010  ndisj2  42104  ndmaovcom  44189  eliunxp2  45162  mpomptx2  45163  i0oii  45665  io1ii  45666  alimp-no-surprise  45807  alsi-no-surprise  45822