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  1513  sbrimvlem  2098  dfsb7OLD  2282  2eu4  2716  2eu5  2717  2eu5OLD  2718  euxfrw  3660  euxfr  3662  euind  3663  rmo4  3669  rmo3f  3673  2reu5lem3  3696  rmo3  3818  difin  4188  axsepgfromrep  5165  reusv2lem4  5267  rabxp  5564  elvvv  5591  eliunxp  5672  elidinxp  5878  imadisj  5915  idrefALT  5940  intirr  5945  resco  6070  funcnv3  6394  fncnv  6397  fun11  6398  fununi  6399  mptfnf  6455  f1mpt  6997  mpomptx  7244  uniuni  7464  frxp  7803  oeeu  8212  ixp0x  8473  xpcomco  8590  1sdom  8705  dffi3  8879  wemapsolem  8998  cardval3  9365  kmlem4  9564  kmlem12  9572  kmlem14  9574  kmlem15  9575  kmlem16  9576  fpwwe2  10054  axgroth4  10243  ltexprlem4  10450  bitsmod  15775  pythagtrip  16161  isstruct  16488  pgpfac1  19195  pgpfac  19199  isassa  20545  basdif0  21558  ntreq0  21682  tgcmp  22006  tx1cn  22214  rnelfmlem  22557  phtpcer  23600  iscvsp  23733  caucfil  23887  minveclem1  24028  ovoliunlem1  24106  mdegleb  24665  istrkg2ld  26254  numedglnl  26937  usgr2pth0  27554  adjbd1o  29868  nelbOLD  30239  nmo  30261  dmrab  30267  difrab2  30268  mpomptxf  30442  ccfldextdgrr  31145  isros  31537  1stmbfm  31628  bnj976  32159  bnj1143  32172  bnj1533  32234  bnj864  32304  bnj983  32333  bnj1174  32385  bnj1175  32386  bnj1280  32402  cvmlift2lem12  32674  axacprim  33046  dmscut  33385  dfrecs2  33524  andnand1  33862  bj-snglc  34405  bj-disj2r  34464  bj-dfmpoa  34533  bj-mpomptALT  34534  mptsnunlem  34755  wl-df3xor2  34886  wl-df4-3mintru2  34904  wl-cases2-dnf  34917  wl-euae  34922  wl-dfralv  35006  itg2addnc  35111  asindmre  35140  brres2  35689  brxrn2  35787  dfxrn2  35788  inxpxrn  35803  refsymrel2  35963  refsymrel3  35964  dfeqvrel2  35985  dfeqvrel3  35986  isopos  36476  dihglblem6  38636  dihglb2  38638  fgraphopab  40154  ifpid2g  40201  ifpim23g  40203  rp-fakeanorass  40221  en2pr  40246  elmapintrab  40276  relnonrel  40287  undmrnresiss  40304  elintima  40354  relexp0eq  40402  iunrelexp0  40403  dffrege115  40679  frege131  40695  frege133  40697  ntrneikb  40797  onfrALTlem5  41248  onfrALTlem5VD  41591  ndisj2  41685  ndmaovcom  43761  eliunxp2  44735  mpomptx2  44736  alimp-no-surprise  45309  alsi-no-surprise  45324