Theorem 3bitr2i 302

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

This proof depends on syntax axioms:   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  con2bi  356  xorneg2  1551  sbrimvwOLD  2129  2eu4  2681  2eu5  2682  r19.41v  3194  r3ex  3203  r19.41  3268  sbralie  3340  sbralieOLD  3342  pm13.183  3623  euxfrw  3682  euxfr  3684  euind  3685  rmo4  3691  rmo3f  3695  2reu5lem3  3718  rmo3  3839  difin  4221  indifdi  4243  dftr5  5220  axsepgfromrep  5253  inuni  5318  reusv2lem4  5370  rabxp  5707  elvvv  5735  eliunxp  5821  elidinxp  6044  imadisj  6080  idrefALT  6111  intirr  6116  resco  6250  funcnv3  6607  fncnv  6610  fun11  6611  fununi  6612  mptfnf  6671  f1mpt  7262  mpomptx  7530  uniuni  7765  frxp  8128  xpord2pred  8147  xpord2indlem  8149  oeeu  8595  ixp0x  8937  xpcomco  9069  dffi3  9405  wemapsolem  9526  karden  9902  cardval3  9961  kmlem4  10160  kmlem12  10168  kmlem14  10170  kmlem15  10171  kmlem16  10172  fpwwe2  10656  axgroth4  10845  ltexprlem4  11052  bitsmod  16532  pythagtrip  16932  isstruct  17250  pgpfac1  20215  pgpfac  20219  basdif0  23184  ntreq0  23308  tgcmp  23632  tx1cn  23841  rnelfmlem  24184  phtpcer  25229  iscvsp  25362  caucfil  25517  minveclem1  25658  ovoliunlem1  25736  mdegleb  26296  eqcuts2  28059  dmcuts  28064  made0  28136  mulsuniflem  28422  istrkg2ld  28809  numedglnl  29609  usgr2pth0  30238  adjbd1o  32574  nmo  32973  dmrab  32980  difrab2  32981  mpomptxf  33159  ccfldextdgrr  34190  fldextrspunlsplem  34191  isros  34687  1stmbfm  34779  bnj976  35295  bnj1143  35307  bnj1533  35369  bnj864  35439  bnj983  35468  bnj1174  35520  bnj1175  35521  bnj1280  35537  axregs  35673  onvf1odlem2  35709  cvmlift2lem12  35901  axacprim  36294  dfrecs2  36537  andnand1  37028  mh-infprim1bi  37173  bj-snglc  37721  bj-disj2r  37780  bj-dfmpoa  37876  bj-mpomptALT  37877  mptsnunlem  38100  wl-df3xor2  38231  wl-df4-3mintru2  38249  wl-cases2-dnf  38283  wl-euae  38288  itg2addnc  38431  asindmre  38460  brres2  39029  brxrn2  39140  dfxrn2  39141  inxpxrn  39174  dfsuccl4  39230  refsymrel2  39407  refsymrel3  39408  dfeqvrel2  39430  dfeqvrel3  39431  isopos  40061  dihglblem6  42221  dihglb2  42223  fgraphopab  44052  unielss  44067  dflim5  44178  ifpid2g  44341  ifpim23g  44343  rp-fakeanorass  44361  en2pr  44395  elmapintrab  44424  relnonrel  44435  undmrnresiss  44452  elintima  44501  relexp0eq  44549  iunrelexp0  44550  dffrege115  44826  frege131  44842  frege133  44844  ntrneikb  44942  elnev  45269  onfrALTlem5  45373  onfrALTlem5VD  45715  ndisj2  45893  ndmaovcom  48101  usgrexmpl2nb3  48958  eliunxp2  49272  mpomptx2  49273  mo0sn  49752  i0oii  49854  io1ii  49855  alimp-no-surprise  50718  als-no-surprise  50743