Theorem 3bitr2i 299

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

Syntax hints:   ↔ 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:  con2bi  353  xorneg2  1518  sbrimvw  2091  2eu4  2658  2eu5  2659  r19.41v  3195  r3ex  3204  r19.41  3269  sbralie  3366  pm13.183  3679  euxfrw  3743  euxfr  3745  euind  3746  rmo4  3752  rmo3f  3756  2reu5lem3  3779  rmo3  3911  difin  4291  indifdi  4313  ab0orv  4406  dftr5  5287  axsepgfromrep  5315  inuni  5368  reusv2lem4  5419  rabxp  5748  elvvv  5775  eliunxp  5862  elidinxp  6073  imadisj  6109  idrefALT  6143  intirr  6150  resco  6281  funcnv3  6648  fncnv  6651  fun11  6652  fununi  6653  mptfnf  6715  f1mpt  7298  mpomptx  7563  uniuni  7797  frxp  8167  xpord2pred  8186  xpord2indlem  8188  oeeu  8659  ixp0x  8984  xpcomco  9128  1sdomOLD  9312  dffi3  9500  wemapsolem  9619  cardval3  10021  kmlem4  10223  kmlem12  10231  kmlem14  10233  kmlem15  10234  kmlem16  10235  fpwwe2  10712  axgroth4  10901  ltexprlem4  11108  bitsmod  16482  pythagtrip  16881  isstruct  17199  pgpfac1  20124  pgpfac  20128  basdif0  22981  ntreq0  23106  tgcmp  23430  tx1cn  23638  rnelfmlem  23981  phtpcer  25046  iscvsp  25180  caucfil  25336  minveclem1  25477  ovoliunlem1  25556  mdegleb  26123  eqscut2  27869  dmscut  27874  made0  27930  mulsuniflem  28193  istrkg2ld  28486  numedglnl  29179  usgr2pth0  29801  adjbd1o  32117  nmo  32518  dmrab  32525  difrab2  32526  mpomptxf  32695  ccfldextdgrr  33682  isros  34132  1stmbfm  34225  bnj976  34753  bnj1143  34766  bnj1533  34828  bnj864  34898  bnj983  34927  bnj1174  34979  bnj1175  34980  bnj1280  34996  cvmlift2lem12  35282  axacprim  35669  dfrecs2  35914  andnand1  36367  bj-snglc  36935  bj-disj2r  36994  bj-dfmpoa  37084  bj-mpomptALT  37085  mptsnunlem  37304  wl-df3xor2  37435  wl-df4-3mintru2  37453  wl-cases2-dnf  37466  wl-euae  37471  itg2addnc  37634  asindmre  37663  brres2  38224  brxrn2  38331  dfxrn2  38332  inxpxrn  38351  refsymrel2  38523  refsymrel3  38524  dfeqvrel2  38546  dfeqvrel3  38547  isopos  39136  dihglblem6  41297  dihglb2  41299  fgraphopab  43164  unielss  43179  dflim5  43291  ifpid2g  43455  ifpim23g  43457  rp-fakeanorass  43475  en2pr  43509  elmapintrab  43538  relnonrel  43549  undmrnresiss  43566  elintima  43615  relexp0eq  43663  iunrelexp0  43664  dffrege115  43940  frege131  43956  frege133  43958  ntrneikb  44056  elnev  44407  onfrALTlem5  44513  onfrALTlem5VD  44856  ndisj2  44953  ndmaovcom  47120  usgrexmpl2nb3  47849  eliunxp2  48058  mpomptx2  48059  mo0sn  48547  i0oii  48599  io1ii  48600  alimp-no-surprise  48875  alsi-no-surprise  48890