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 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  353  xorneg2  1514  sbrimvw  2086  2eu4  2642  2eu5  2643  sbralie  3346  euxfrw  3709  euxfr  3711  euind  3712  rmo4  3718  rmo3f  3722  2reu5lem3  3745  rmo3  3875  difin  4253  indifdi  4275  ab0orv  4370  dftr5  5259  axsepgfromrep  5287  reusv2lem4  5389  rabxp  5714  elvvv  5741  eliunxp  5827  elidinxp  6033  imadisj  6069  idrefALT  6102  intirr  6109  resco  6239  funcnv3  6608  fncnv  6611  fun11  6612  fununi  6613  mptfnf  6675  f1mpt  7252  mpomptx  7513  uniuni  7742  frxp  8106  xpord2pred  8125  xpord2indlem  8127  oeeu  8598  ixp0x  8915  xpcomco  9057  1sdomOLD  9244  dffi3  9421  wemapsolem  9540  cardval3  9942  kmlem4  10143  kmlem12  10151  kmlem14  10153  kmlem15  10154  kmlem16  10155  fpwwe2  10633  axgroth4  10822  ltexprlem4  11029  bitsmod  16373  pythagtrip  16763  isstruct  17081  pgpfac1  19987  pgpfac  19991  basdif0  22766  ntreq0  22891  tgcmp  23215  tx1cn  23423  rnelfmlem  23766  phtpcer  24831  iscvsp  24965  caucfil  25121  minveclem1  25262  ovoliunlem1  25341  mdegleb  25910  eqscut2  27643  dmscut  27648  made0  27704  mulsuniflem  27953  istrkg2ld  28135  numedglnl  28828  usgr2pth0  29446  adjbd1o  31762  nmo  32154  dmrab  32161  difrab2  32162  mpomptxf  32329  ccfldextdgrr  33192  isros  33621  1stmbfm  33714  bnj976  34243  bnj1143  34256  bnj1533  34318  bnj864  34388  bnj983  34417  bnj1174  34469  bnj1175  34470  bnj1280  34486  cvmlift2lem12  34760  axacprim  35137  dfrecs2  35383  andnand1  35742  bj-snglc  36306  bj-disj2r  36365  bj-dfmpoa  36455  bj-mpomptALT  36456  mptsnunlem  36675  wl-df3xor2  36806  wl-df4-3mintru2  36824  wl-cases2-dnf  36837  wl-euae  36842  itg2addnc  36998  asindmre  37027  brres2  37592  brxrn2  37701  dfxrn2  37702  inxpxrn  37721  refsymrel2  37893  refsymrel3  37894  dfeqvrel2  37916  dfeqvrel3  37917  isopos  38506  dihglblem6  40667  dihglb2  40669  fgraphopab  42407  unielss  42422  dflim5  42534  ifpid2g  42699  ifpim23g  42701  rp-fakeanorass  42719  en2pr  42753  elmapintrab  42782  relnonrel  42793  undmrnresiss  42810  elintima  42859  relexp0eq  42907  iunrelexp0  42908  dffrege115  43184  frege131  43200  frege133  43202  ntrneikb  43300  elnev  43652  onfrALTlem5  43758  onfrALTlem5VD  44101  ndisj2  44192  ndmaovcom  46364  eliunxp2  47164  mpomptx2  47165  mo0sn  47654  i0oii  47706  io1ii  47707  alimp-no-surprise  47982  alsi-no-surprise  47997