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

Syntax hints:   ↔ wb 205

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 206

This theorem is referenced by:  con2bi  354  xorneg2  1517  sbrimvw  2095  2eu4  2657  2eu5  2658  euxfrw  3657  euxfr  3659  euind  3660  rmo4  3666  rmo3f  3670  2reu5lem3  3693  rmo3  3823  difin  4196  indifdi  4218  ab0orv  4313  axsepgfromrep  5222  reusv2lem4  5325  rabxp  5636  elvvv  5663  eliunxp  5749  elidinxp  5954  imadisj  5991  idrefALT  6023  intirr  6028  resco  6158  funcnv3  6511  fncnv  6514  fun11  6515  fununi  6516  mptfnf  6577  f1mpt  7143  mpomptx  7396  uniuni  7621  frxp  7976  oeeu  8443  ixp0x  8723  xpcomco  8858  1sdom  9034  dffi3  9199  wemapsolem  9318  cardval3  9719  kmlem4  9918  kmlem12  9926  kmlem14  9928  kmlem15  9929  kmlem16  9930  fpwwe2  10408  axgroth4  10597  ltexprlem4  10804  bitsmod  16152  pythagtrip  16544  isstruct  16862  pgpfac1  19692  pgpfac  19696  isassa  21072  basdif0  22112  ntreq0  22237  tgcmp  22561  tx1cn  22769  rnelfmlem  23112  phtpcer  24167  iscvsp  24300  caucfil  24456  minveclem1  24597  ovoliunlem1  24675  mdegleb  25238  istrkg2ld  26830  numedglnl  27523  usgr2pth0  28142  adjbd1o  30456  nelbOLDOLD  30826  nmo  30847  dmrab  30853  difrab2  30854  mpomptxf  31025  ccfldextdgrr  31751  isros  32145  1stmbfm  32236  bnj976  32766  bnj1143  32779  bnj1533  32841  bnj864  32911  bnj983  32940  bnj1174  32992  bnj1175  32993  bnj1280  33009  cvmlift2lem12  33285  axacprim  33657  xpord2pred  33801  xpord2ind  33803  eqscut2  34009  dmscut  34014  made0  34066  dfrecs2  34261  andnand1  34599  bj-snglc  35168  bj-disj2r  35227  bj-dfmpoa  35298  bj-mpomptALT  35299  mptsnunlem  35518  wl-df3xor2  35649  wl-df4-3mintru2  35667  wl-cases2-dnf  35680  wl-euae  35685  itg2addnc  35840  asindmre  35869  brres2  36415  brxrn2  36512  dfxrn2  36513  inxpxrn  36528  refsymrel2  36688  refsymrel3  36689  dfeqvrel2  36710  dfeqvrel3  36711  isopos  37201  dihglblem6  39361  dihglb2  39363  fgraphopab  41042  ifpid2g  41107  ifpim23g  41109  rp-fakeanorass  41127  en2pr  41161  elmapintrab  41191  relnonrel  41202  undmrnresiss  41219  elintima  41268  relexp0eq  41316  iunrelexp0  41317  dffrege115  41593  frege131  41609  frege133  41611  ntrneikb  41711  onfrALTlem5  42169  onfrALTlem5VD  42512  ndisj2  42606  ndmaovcom  44708  eliunxp2  45680  mpomptx2  45681  mo0sn  46172  i0oii  46224  io1ii  46225  alimp-no-surprise  46496  alsi-no-surprise  46511