Theorem 3bitr2i 300

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

Syntax hints:   ↔ wb 207

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 208

This theorem is referenced by:  con2bi  354  xorneg2  1528  sbrimvw  2102  2eu4  2659  2eu5  2660  r19.41v  3170  r3ex  3179  r19.41  3244  sbralie  3318  sbralieOLD  3320  pm13.183  3611  euxfrw  3669  euxfr  3671  euind  3672  rmo4  3678  rmo3f  3682  2reu5lem3  3705  rmo3  3828  difin  4207  indifdi  4229  dftr5  5190  axsepgfromrep  5223  inuni  5285  reusv2lem4  5337  rabxp  5673  elvvv  5701  eliunxp  5786  elidinxp  6003  imadisj  6039  idrefALT  6070  intirr  6075  resco  6208  funcnv3  6562  fncnv  6565  fun11  6566  fununi  6567  mptfnf  6627  f1mpt  7212  mpomptx  7476  uniuni  7712  frxp  8073  xpord2pred  8092  xpord2indlem  8094  oeeu  8536  ixp0x  8871  xpcomco  9002  dffi3  9341  wemapsolem  9462  cardval3  9874  kmlem4  10074  kmlem12  10082  kmlem14  10084  kmlem15  10085  kmlem16  10086  fpwwe2  10564  axgroth4  10753  ltexprlem4  10960  bitsmod  16403  pythagtrip  16803  isstruct  17120  pgpfac1  20055  pgpfac  20059  basdif0  22943  ntreq0  23067  tgcmp  23391  tx1cn  23599  rnelfmlem  23942  phtpcer  24987  iscvsp  25120  caucfil  25275  minveclem1  25416  ovoliunlem1  25494  mdegleb  26054  eqcuts2  27803  dmcuts  27808  made0  27880  mulsuniflem  28166  istrkg2ld  28553  numedglnl  29238  usgr2pth0  29858  adjbd1o  32181  nmo  32584  dmrab  32591  difrab2  32592  mpomptxf  32777  ccfldextdgrr  33863  fldextrspunlsplem  33864  isros  34359  1stmbfm  34451  bnj976  34967  bnj1143  34979  bnj1533  35041  bnj864  35111  bnj983  35140  bnj1174  35192  bnj1175  35193  bnj1280  35209  axregs  35327  onvf1odlem2  35339  cvmlift2lem12  35549  axacprim  35942  dfrecs2  36185  andnand1  36636  mh-infprim1bi  36781  bj-snglc  37329  bj-disj2r  37388  bj-dfmpoa  37483  bj-mpomptALT  37484  mptsnunlem  37707  wl-df3xor2  37838  wl-df4-3mintru2  37856  wl-cases2-dnf  37890  wl-euae  37895  itg2addnc  38048  asindmre  38077  brres2  38647  brxrn2  38758  dfxrn2  38759  inxpxrn  38792  dfsuccl4  38848  refsymrel2  39025  refsymrel3  39026  dfeqvrel2  39048  dfeqvrel3  39049  isopos  39679  dihglblem6  41839  dihglb2  41841  fgraphopab  43655  unielss  43670  dflim5  43781  ifpid2g  43944  ifpim23g  43946  rp-fakeanorass  43964  en2pr  43998  elmapintrab  44027  relnonrel  44038  undmrnresiss  44055  elintima  44104  relexp0eq  44152  iunrelexp0  44153  dffrege115  44429  frege131  44445  frege133  44447  ntrneikb  44545  elnev  44888  onfrALTlem5  44993  onfrALTlem5VD  45335  ndisj2  45506  ndmaovcom  47675  usgrexmpl2nb3  48532  eliunxp2  48832  mpomptx2  48833  mo0sn  49313  i0oii  49417  io1ii  49418  alimp-no-surprise  50278  alsi-no-surprise  50293