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  1523  sbrimvw  2097  2eu4  2656  2eu5  2657  r19.41v  3168  r3ex  3177  r19.41  3242  sbralie  3324  sbralieOLD  3326  pm13.183  3622  euxfrw  3681  euxfr  3683  euind  3684  rmo4  3690  rmo3f  3694  2reu5lem3  3717  rmo3  3841  difin  4226  indifdi  4248  dftr5  5211  axsepgfromrep  5241  inuni  5297  reusv2lem4  5348  rabxp  5680  elvvv  5708  eliunxp  5794  elidinxp  6011  imadisj  6047  idrefALT  6078  intirr  6083  resco  6216  funcnv3  6570  fncnv  6573  fun11  6574  fununi  6575  mptfnf  6635  f1mpt  7217  mpomptx  7481  uniuni  7717  frxp  8078  xpord2pred  8097  xpord2indlem  8099  oeeu  8541  ixp0x  8876  xpcomco  9007  dffi3  9346  wemapsolem  9467  cardval3  9876  kmlem4  10076  kmlem12  10084  kmlem14  10086  kmlem15  10087  kmlem16  10088  fpwwe2  10566  axgroth4  10755  ltexprlem4  10962  bitsmod  16375  pythagtrip  16774  isstruct  17091  pgpfac1  20023  pgpfac  20027  basdif0  22909  ntreq0  23033  tgcmp  23357  tx1cn  23565  rnelfmlem  23908  phtpcer  24962  iscvsp  25096  caucfil  25251  minveclem1  25392  ovoliunlem1  25471  mdegleb  26037  eqcuts2  27794  dmcuts  27799  made0  27871  mulsuniflem  28157  istrkg2ld  28544  numedglnl  29229  usgr2pth0  29850  adjbd1o  32172  nmo  32575  dmrab  32582  difrab2  32583  mpomptxf  32767  ccfldextdgrr  33849  fldextrspunlsplem  33850  isros  34345  1stmbfm  34437  bnj976  34953  bnj1143  34965  bnj1533  35027  bnj864  35097  bnj983  35126  bnj1174  35178  bnj1175  35179  bnj1280  35195  axregs  35314  onvf1odlem2  35317  cvmlift2lem12  35527  axacprim  35920  dfrecs2  36163  andnand1  36614  bj-snglc  37214  bj-disj2r  37273  bj-dfmpoa  37368  bj-mpomptALT  37369  mptsnunlem  37590  wl-df3xor2  37721  wl-df4-3mintru2  37739  wl-cases2-dnf  37764  wl-euae  37769  itg2addnc  37922  asindmre  37951  brres2  38521  brxrn2  38632  dfxrn2  38633  inxpxrn  38666  dfsuccl4  38722  refsymrel2  38899  refsymrel3  38900  dfeqvrel2  38922  dfeqvrel3  38923  isopos  39553  dihglblem6  41713  dihglb2  41715  fgraphopab  43557  unielss  43572  dflim5  43683  ifpid2g  43846  ifpim23g  43848  rp-fakeanorass  43866  en2pr  43900  elmapintrab  43929  relnonrel  43940  undmrnresiss  43957  elintima  44006  relexp0eq  44054  iunrelexp0  44055  dffrege115  44331  frege131  44347  frege133  44349  ntrneikb  44447  elnev  44790  onfrALTlem5  44895  onfrALTlem5VD  45237  ndisj2  45408  ndmaovcom  47562  usgrexmpl2nb3  48391  eliunxp2  48691  mpomptx2  48692  mo0sn  49172  i0oii  49276  io1ii  49277  alimp-no-surprise  50137  alsi-no-surprise  50152