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  1522  sbrimvw  2094  2eu4  2650  2eu5  2651  r19.41v  3162  r3ex  3171  r19.41  3236  sbralie  3318  sbralieOLD  3320  pm13.183  3621  euxfrw  3680  euxfr  3682  euind  3683  rmo4  3689  rmo3f  3693  2reu5lem3  3716  rmo3  3840  difin  4222  indifdi  4244  ab0orv  4333  dftr5  5202  axsepgfromrep  5232  inuni  5288  reusv2lem4  5339  rabxp  5664  elvvv  5692  eliunxp  5777  elidinxp  5993  imadisj  6029  idrefALT  6060  intirr  6065  resco  6197  funcnv3  6551  fncnv  6554  fun11  6555  fununi  6556  mptfnf  6616  f1mpt  7195  mpomptx  7459  uniuni  7695  frxp  8056  xpord2pred  8075  xpord2indlem  8077  oeeu  8518  ixp0x  8850  xpcomco  8980  dffi3  9315  wemapsolem  9436  cardval3  9845  kmlem4  10045  kmlem12  10053  kmlem14  10055  kmlem15  10056  kmlem16  10057  fpwwe2  10534  axgroth4  10723  ltexprlem4  10930  bitsmod  16347  pythagtrip  16746  isstruct  17063  pgpfac1  19995  pgpfac  19999  basdif0  22869  ntreq0  22993  tgcmp  23317  tx1cn  23525  rnelfmlem  23868  phtpcer  24922  iscvsp  25056  caucfil  25211  minveclem1  25352  ovoliunlem1  25431  mdegleb  25997  eqscut2  27748  dmscut  27753  made0  27819  mulsuniflem  28089  istrkg2ld  28439  numedglnl  29123  usgr2pth0  29744  adjbd1o  32063  nmo  32467  dmrab  32474  difrab2  32475  mpomptxf  32657  ccfldextdgrr  33683  fldextrspunlsplem  33684  isros  34179  1stmbfm  34271  bnj976  34787  bnj1143  34800  bnj1533  34862  bnj864  34932  bnj983  34961  bnj1174  35013  bnj1175  35014  bnj1280  35030  axregs  35143  onvf1odlem2  35146  cvmlift2lem12  35356  axacprim  35749  dfrecs2  35990  andnand1  36441  bj-snglc  37009  bj-disj2r  37068  bj-dfmpoa  37158  bj-mpomptALT  37159  mptsnunlem  37378  wl-df3xor2  37509  wl-df4-3mintru2  37527  wl-cases2-dnf  37552  wl-euae  37557  itg2addnc  37720  asindmre  37749  brres2  38309  brxrn2  38409  dfxrn2  38410  inxpxrn  38433  refsymrel2  38610  refsymrel3  38611  dfeqvrel2  38633  dfeqvrel3  38634  isopos  39225  dihglblem6  41385  dihglb2  41387  fgraphopab  43242  unielss  43257  dflim5  43368  ifpid2g  43532  ifpim23g  43534  rp-fakeanorass  43552  en2pr  43586  elmapintrab  43615  relnonrel  43626  undmrnresiss  43643  elintima  43692  relexp0eq  43740  iunrelexp0  43741  dffrege115  44017  frege131  44033  frege133  44035  ntrneikb  44133  elnev  44476  onfrALTlem5  44581  onfrALTlem5VD  44923  ndisj2  45094  ndmaovcom  47242  usgrexmpl2nb3  48071  eliunxp2  48371  mpomptx2  48372  mo0sn  48853  i0oii  48957  io1ii  48958  alimp-no-surprise  49819  alsi-no-surprise  49834