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  1523  sbrimvw  2097  2eu4  2655  2eu5  2656  r19.41v  3167  r3ex  3176  r19.41  3241  sbralie  3315  sbralieOLD  3317  pm13.183  3608  euxfrw  3667  euxfr  3669  euind  3670  rmo4  3676  rmo3f  3680  2reu5lem3  3703  rmo3  3827  difin  4212  indifdi  4234  dftr5  5196  axsepgfromrep  5229  inuni  5291  reusv2lem4  5343  rabxp  5679  elvvv  5707  eliunxp  5792  elidinxp  6009  imadisj  6045  idrefALT  6076  intirr  6081  resco  6214  funcnv3  6568  fncnv  6571  fun11  6572  fununi  6573  mptfnf  6633  f1mpt  7216  mpomptx  7480  uniuni  7716  frxp  8076  xpord2pred  8095  xpord2indlem  8097  oeeu  8539  ixp0x  8874  xpcomco  9005  dffi3  9344  wemapsolem  9465  cardval3  9876  kmlem4  10076  kmlem12  10084  kmlem14  10086  kmlem15  10087  kmlem16  10088  fpwwe2  10566  axgroth4  10755  ltexprlem4  10962  bitsmod  16405  pythagtrip  16805  isstruct  17122  pgpfac1  20057  pgpfac  20061  basdif0  22918  ntreq0  23042  tgcmp  23366  tx1cn  23574  rnelfmlem  23917  phtpcer  24962  iscvsp  25095  caucfil  25250  minveclem1  25391  ovoliunlem1  25469  mdegleb  26029  eqcuts2  27778  dmcuts  27783  made0  27855  mulsuniflem  28141  istrkg2ld  28528  numedglnl  29213  usgr2pth0  29833  adjbd1o  32156  nmo  32559  dmrab  32566  difrab2  32567  mpomptxf  32751  ccfldextdgrr  33816  fldextrspunlsplem  33817  isros  34312  1stmbfm  34404  bnj976  34920  bnj1143  34932  bnj1533  34994  bnj864  35064  bnj983  35093  bnj1174  35145  bnj1175  35146  bnj1280  35162  axregs  35283  onvf1odlem2  35286  cvmlift2lem12  35496  axacprim  35889  dfrecs2  36132  andnand1  36583  mh-infprim1bi  36728  bj-snglc  37276  bj-disj2r  37335  bj-dfmpoa  37430  bj-mpomptALT  37431  mptsnunlem  37654  wl-df3xor2  37785  wl-df4-3mintru2  37803  wl-cases2-dnf  37837  wl-euae  37842  itg2addnc  37995  asindmre  38024  brres2  38594  brxrn2  38705  dfxrn2  38706  inxpxrn  38739  dfsuccl4  38795  refsymrel2  38972  refsymrel3  38973  dfeqvrel2  38995  dfeqvrel3  38996  isopos  39626  dihglblem6  41786  dihglb2  41788  fgraphopab  43631  unielss  43646  dflim5  43757  ifpid2g  43920  ifpim23g  43922  rp-fakeanorass  43940  en2pr  43974  elmapintrab  44003  relnonrel  44014  undmrnresiss  44031  elintima  44080  relexp0eq  44128  iunrelexp0  44129  dffrege115  44405  frege131  44421  frege133  44423  ntrneikb  44521  elnev  44864  onfrALTlem5  44969  onfrALTlem5VD  45311  ndisj2  45482  ndmaovcom  47653  usgrexmpl2nb3  48510  eliunxp2  48810  mpomptx2  48811  mo0sn  49291  i0oii  49395  io1ii  49396  alimp-no-surprise  50256  alsi-no-surprise  50271