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  1521  sbrimvw  2092  2eu4  2648  2eu5  2649  r19.41v  3167  r3ex  3176  r19.41  3241  sbralie  3326  sbralieOLD  3328  pm13.183  3632  euxfrw  3692  euxfr  3694  euind  3695  rmo4  3701  rmo3f  3705  2reu5lem3  3728  rmo3  3852  difin  4235  indifdi  4257  ab0orv  4346  dftr5  5218  axsepgfromrep  5249  inuni  5305  reusv2lem4  5356  rabxp  5686  elvvv  5714  eliunxp  5801  elidinxp  6015  imadisj  6051  idrefALT  6084  intirr  6091  resco  6223  funcnv3  6586  fncnv  6589  fun11  6590  fununi  6591  mptfnf  6653  f1mpt  7236  mpomptx  7502  uniuni  7738  frxp  8105  xpord2pred  8124  xpord2indlem  8126  oeeu  8567  ixp0x  8899  xpcomco  9031  1sdomOLD  9196  dffi3  9382  wemapsolem  9503  cardval3  9905  kmlem4  10107  kmlem12  10115  kmlem14  10117  kmlem15  10118  kmlem16  10119  fpwwe2  10596  axgroth4  10785  ltexprlem4  10992  bitsmod  16406  pythagtrip  16805  isstruct  17122  pgpfac1  20012  pgpfac  20016  basdif0  22840  ntreq0  22964  tgcmp  23288  tx1cn  23496  rnelfmlem  23839  phtpcer  24894  iscvsp  25028  caucfil  25183  minveclem1  25324  ovoliunlem1  25403  mdegleb  25969  eqscut2  27718  dmscut  27723  made0  27785  mulsuniflem  28052  istrkg2ld  28387  numedglnl  29071  usgr2pth0  29695  adjbd1o  32014  nmo  32419  dmrab  32426  difrab2  32427  mpomptxf  32601  ccfldextdgrr  33667  fldextrspunlsplem  33668  isros  34158  1stmbfm  34251  bnj976  34767  bnj1143  34780  bnj1533  34842  bnj864  34912  bnj983  34941  bnj1174  34993  bnj1175  34994  bnj1280  35010  onvf1odlem2  35091  cvmlift2lem12  35301  axacprim  35694  dfrecs2  35938  andnand1  36389  bj-snglc  36957  bj-disj2r  37016  bj-dfmpoa  37106  bj-mpomptALT  37107  mptsnunlem  37326  wl-df3xor2  37457  wl-df4-3mintru2  37475  wl-cases2-dnf  37500  wl-euae  37505  itg2addnc  37668  asindmre  37697  brres2  38257  brxrn2  38357  dfxrn2  38358  inxpxrn  38381  refsymrel2  38558  refsymrel3  38559  dfeqvrel2  38581  dfeqvrel3  38582  isopos  39173  dihglblem6  41334  dihglb2  41336  fgraphopab  43192  unielss  43207  dflim5  43318  ifpid2g  43482  ifpim23g  43484  rp-fakeanorass  43502  en2pr  43536  elmapintrab  43565  relnonrel  43576  undmrnresiss  43593  elintima  43642  relexp0eq  43690  iunrelexp0  43691  dffrege115  43967  frege131  43983  frege133  43985  ntrneikb  44083  elnev  44427  onfrALTlem5  44532  onfrALTlem5VD  44874  ndisj2  45045  ndmaovcom  47203  usgrexmpl2nb3  48022  eliunxp2  48319  mpomptx2  48320  mo0sn  48801  i0oii  48905  io1ii  48906  alimp-no-surprise  49767  alsi-no-surprise  49782