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  354  xorneg2  1521  sbrimvw  2095  2eu4  2651  2eu5  2652  sbralie  3355  euxfrw  3718  euxfr  3720  euind  3721  rmo4  3727  rmo3f  3731  2reu5lem3  3754  rmo3  3884  difin  4262  indifdi  4284  ab0orv  4379  dftr5  5270  axsepgfromrep  5298  reusv2lem4  5400  rabxp  5725  elvvv  5752  eliunxp  5838  elidinxp  6044  imadisj  6080  idrefALT  6113  intirr  6120  resco  6250  funcnv3  6619  fncnv  6622  fun11  6623  fununi  6624  mptfnf  6686  f1mpt  7260  mpomptx  7521  uniuni  7749  frxp  8112  xpord2pred  8131  xpord2indlem  8133  oeeu  8603  ixp0x  8920  xpcomco  9062  1sdomOLD  9249  dffi3  9426  wemapsolem  9545  cardval3  9947  kmlem4  10148  kmlem12  10156  kmlem14  10158  kmlem15  10159  kmlem16  10160  fpwwe2  10638  axgroth4  10827  ltexprlem4  11034  bitsmod  16377  pythagtrip  16767  isstruct  17085  pgpfac1  19950  pgpfac  19954  basdif0  22456  ntreq0  22581  tgcmp  22905  tx1cn  23113  rnelfmlem  23456  phtpcer  24511  iscvsp  24644  caucfil  24800  minveclem1  24941  ovoliunlem1  25019  mdegleb  25582  eqscut2  27308  dmscut  27313  made0  27369  mulsuniflem  27607  istrkg2ld  27742  numedglnl  28435  usgr2pth0  29053  adjbd1o  31369  nmo  31761  dmrab  31768  difrab2  31769  mpomptxf  31936  ccfldextdgrr  32777  isros  33197  1stmbfm  33290  bnj976  33819  bnj1143  33832  bnj1533  33894  bnj864  33964  bnj983  33993  bnj1174  34045  bnj1175  34046  bnj1280  34062  cvmlift2lem12  34336  axacprim  34707  dfrecs2  34953  andnand1  35334  bj-snglc  35898  bj-disj2r  35957  bj-dfmpoa  36047  bj-mpomptALT  36048  mptsnunlem  36267  wl-df3xor2  36398  wl-df4-3mintru2  36416  wl-cases2-dnf  36429  wl-euae  36434  itg2addnc  36590  asindmre  36619  brres2  37184  brxrn2  37293  dfxrn2  37294  inxpxrn  37313  refsymrel2  37485  refsymrel3  37486  dfeqvrel2  37508  dfeqvrel3  37509  isopos  38098  dihglblem6  40259  dihglb2  40261  fgraphopab  42000  unielss  42015  dflim5  42127  ifpid2g  42292  ifpim23g  42294  rp-fakeanorass  42312  en2pr  42346  elmapintrab  42375  relnonrel  42386  undmrnresiss  42403  elintima  42452  relexp0eq  42500  iunrelexp0  42501  dffrege115  42777  frege131  42793  frege133  42795  ntrneikb  42893  elnev  43245  onfrALTlem5  43351  onfrALTlem5VD  43694  ndisj2  43786  ndmaovcom  45961  eliunxp2  47057  mpomptx2  47058  mo0sn  47548  i0oii  47600  io1ii  47601  alimp-no-surprise  47876  alsi-no-surprise  47891