Theorem 3bitr2i 301

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

Syntax hints:   ↔ wb 208

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 209

This theorem is referenced by:  con2bi  355  xorneg2  1540  sbrimvwOLD  2124  2eu4  2680  2eu5  2681  r19.41v  3191  r3ex  3200  r19.41  3265  sbralie  3339  sbralieOLD  3341  pm13.183  3624  euxfrw  3682  euxfr  3684  euind  3685  rmo4  3691  rmo3f  3695  2reu5lem3  3718  rmo3  3840  difin  4222  indifdi  4244  dftr5  5208  axsepgfromrep  5241  inuni  5303  reusv2lem4  5355  rabxp  5691  elvvv  5719  eliunxp  5805  elidinxp  6028  imadisj  6064  idrefALT  6095  intirr  6100  resco  6231  funcnv3  6585  fncnv  6588  fun11  6589  fununi  6590  mptfnf  6650  f1mpt  7239  mpomptx  7503  uniuni  7739  frxp  8099  xpord2pred  8118  xpord2indlem  8120  oeeu  8566  ixp0x  8901  xpcomco  9032  dffi3  9370  wemapsolem  9491  cardval3  9903  kmlem4  10103  kmlem12  10111  kmlem14  10113  kmlem15  10114  kmlem16  10115  fpwwe2  10594  axgroth4  10783  ltexprlem4  10990  bitsmod  16460  pythagtrip  16860  isstruct  17178  pgpfac1  20112  pgpfac  20116  basdif0  23000  ntreq0  23124  tgcmp  23448  tx1cn  23656  rnelfmlem  23999  phtpcer  25044  iscvsp  25177  caucfil  25332  minveclem1  25473  ovoliunlem1  25551  mdegleb  26111  eqcuts2  27866  dmcuts  27871  made0  27943  mulsuniflem  28229  istrkg2ld  28616  numedglnl  29301  usgr2pth0  29921  adjbd1o  32244  nmo  32647  dmrab  32654  difrab2  32655  mpomptxf  32840  ccfldextdgrr  33929  fldextrspunlsplem  33930  isros  34425  1stmbfm  34517  bnj976  35033  bnj1143  35045  bnj1533  35107  bnj864  35177  bnj983  35206  bnj1174  35258  bnj1175  35259  bnj1280  35275  axregs  35395  onvf1odlem2  35407  cvmlift2lem12  35624  axacprim  36017  dfrecs2  36260  andnand1  36721  mh-infprim1bi  36866  bj-snglc  37414  bj-disj2r  37473  bj-dfmpoa  37568  bj-mpomptALT  37569  mptsnunlem  37792  wl-df3xor2  37923  wl-df4-3mintru2  37941  wl-cases2-dnf  37975  wl-euae  37980  itg2addnc  38133  asindmre  38162  brres2  38732  brxrn2  38843  dfxrn2  38844  inxpxrn  38877  dfsuccl4  38933  refsymrel2  39110  refsymrel3  39111  dfeqvrel2  39133  dfeqvrel3  39134  isopos  39764  dihglblem6  41924  dihglb2  41926  fgraphopab  43740  unielss  43755  dflim5  43866  ifpid2g  44029  ifpim23g  44031  rp-fakeanorass  44049  en2pr  44083  elmapintrab  44112  relnonrel  44123  undmrnresiss  44140  elintima  44189  relexp0eq  44237  iunrelexp0  44238  dffrege115  44514  frege131  44530  frege133  44532  ntrneikb  44630  elnev  44973  onfrALTlem5  45078  onfrALTlem5VD  45420  ndisj2  45591  ndmaovcom  47759  usgrexmpl2nb3  48616  eliunxp2  48916  mpomptx2  48917  mo0sn  49397  i0oii  49501  io1ii  49502  alimp-no-surprise  50362  alsi-no-surprise  50377