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  2685  2eu5  2686  r19.41v  3198  r3ex  3207  r19.41  3272  sbralie  3345  sbralieOLD  3347  pm13.183  3628  euxfrw  3687  euxfr  3689  euind  3690  rmo4  3696  rmo3f  3700  2reu5lem3  3723  rmo3  3845  difin  4228  indifdi  4250  dftr5  5227  axsepgfromrep  5260  inuni  5325  reusv2lem4  5377  rabxp  5714  elvvv  5742  eliunxp  5828  elidinxp  6051  imadisj  6087  idrefALT  6118  intirr  6123  resco  6256  funcnv3  6613  fncnv  6616  fun11  6617  fununi  6618  mptfnf  6677  f1mpt  7266  mpomptx  7536  uniuni  7770  frxp  8131  xpord2pred  8150  xpord2indlem  8152  oeeu  8598  ixp0x  8933  xpcomco  9065  dffi3  9401  wemapsolem  9522  karden  9898  cardval3  9957  kmlem4  10156  kmlem12  10164  kmlem14  10166  kmlem15  10167  kmlem16  10168  fpwwe2  10646  axgroth4  10835  ltexprlem4  11042  bitsmod  16519  pythagtrip  16919  isstruct  17237  pgpfac1  20183  pgpfac  20187  basdif0  23147  ntreq0  23271  tgcmp  23595  tx1cn  23803  rnelfmlem  24146  phtpcer  25191  iscvsp  25324  caucfil  25479  minveclem1  25620  ovoliunlem1  25698  mdegleb  26258  eqcuts2  28016  dmcuts  28021  made0  28093  mulsuniflem  28379  istrkg2ld  28766  numedglnl  29531  usgr2pth0  30151  adjbd1o  32474  nmo  32873  dmrab  32880  difrab2  32881  mpomptxf  33060  ccfldextdgrr  34093  fldextrspunlsplem  34094  isros  34590  1stmbfm  34682  bnj976  35198  bnj1143  35210  bnj1533  35272  bnj864  35342  bnj983  35371  bnj1174  35423  bnj1175  35424  bnj1280  35440  axregs  35576  onvf1odlem2  35612  cvmlift2lem12  35827  axacprim  36220  dfrecs2  36463  andnand1  36953  mh-infprim1bi  37098  bj-snglc  37646  bj-disj2r  37705  bj-dfmpoa  37801  bj-mpomptALT  37802  mptsnunlem  38025  wl-df3xor2  38156  wl-df4-3mintru2  38174  wl-cases2-dnf  38208  wl-euae  38213  itg2addnc  38366  asindmre  38395  brres2  38963  brxrn2  39074  dfxrn2  39075  inxpxrn  39108  dfsuccl4  39164  refsymrel2  39341  refsymrel3  39342  dfeqvrel2  39364  dfeqvrel3  39365  isopos  39995  dihglblem6  42155  dihglb2  42157  fgraphopab  43971  unielss  43986  dflim5  44097  ifpid2g  44260  ifpim23g  44262  rp-fakeanorass  44280  en2pr  44314  elmapintrab  44343  relnonrel  44354  undmrnresiss  44371  elintima  44420  relexp0eq  44468  iunrelexp0  44469  dffrege115  44745  frege131  44761  frege133  44763  ntrneikb  44861  elnev  45188  onfrALTlem5  45292  onfrALTlem5VD  45634  ndisj2  45812  ndmaovcom  47983  usgrexmpl2nb3  48840  eliunxp2  49155  mpomptx2  49156  mo0sn  49635  i0oii  49739  io1ii  49740  alimp-no-surprise  50600  als-no-surprise  50625