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  2656  2eu5  2657  r19.41v  3168  r3ex  3177  r19.41  3242  sbralie  3316  sbralieOLD  3318  pm13.183  3609  euxfrw  3668  euxfr  3670  euind  3671  rmo4  3677  rmo3f  3681  2reu5lem3  3704  rmo3  3828  difin  4213  indifdi  4235  dftr5  5197  axsepgfromrep  5229  inuni  5287  reusv2lem4  5338  rabxp  5672  elvvv  5700  eliunxp  5786  elidinxp  6003  imadisj  6039  idrefALT  6070  intirr  6075  resco  6208  funcnv3  6562  fncnv  6565  fun11  6566  fununi  6567  mptfnf  6627  f1mpt  7209  mpomptx  7473  uniuni  7709  frxp  8069  xpord2pred  8088  xpord2indlem  8090  oeeu  8532  ixp0x  8867  xpcomco  8998  dffi3  9337  wemapsolem  9458  cardval3  9867  kmlem4  10067  kmlem12  10075  kmlem14  10077  kmlem15  10078  kmlem16  10079  fpwwe2  10557  axgroth4  10746  ltexprlem4  10953  bitsmod  16396  pythagtrip  16796  isstruct  17113  pgpfac1  20048  pgpfac  20052  basdif0  22928  ntreq0  23052  tgcmp  23376  tx1cn  23584  rnelfmlem  23927  phtpcer  24972  iscvsp  25105  caucfil  25260  minveclem1  25401  ovoliunlem1  25479  mdegleb  26039  eqcuts2  27792  dmcuts  27797  made0  27869  mulsuniflem  28155  istrkg2ld  28542  numedglnl  29227  usgr2pth0  29848  adjbd1o  32171  nmo  32574  dmrab  32581  difrab2  32582  mpomptxf  32766  ccfldextdgrr  33832  fldextrspunlsplem  33833  isros  34328  1stmbfm  34420  bnj976  34936  bnj1143  34948  bnj1533  35010  bnj864  35080  bnj983  35109  bnj1174  35161  bnj1175  35162  bnj1280  35178  axregs  35299  onvf1odlem2  35302  cvmlift2lem12  35512  axacprim  35905  dfrecs2  36148  andnand1  36599  mh-infprim1bi  36744  bj-snglc  37292  bj-disj2r  37351  bj-dfmpoa  37446  bj-mpomptALT  37447  mptsnunlem  37668  wl-df3xor2  37799  wl-df4-3mintru2  37817  wl-cases2-dnf  37851  wl-euae  37856  itg2addnc  38009  asindmre  38038  brres2  38608  brxrn2  38719  dfxrn2  38720  inxpxrn  38753  dfsuccl4  38809  refsymrel2  38986  refsymrel3  38987  dfeqvrel2  39009  dfeqvrel3  39010  isopos  39640  dihglblem6  41800  dihglb2  41802  fgraphopab  43649  unielss  43664  dflim5  43775  ifpid2g  43938  ifpim23g  43940  rp-fakeanorass  43958  en2pr  43992  elmapintrab  44021  relnonrel  44032  undmrnresiss  44049  elintima  44098  relexp0eq  44146  iunrelexp0  44147  dffrege115  44423  frege131  44439  frege133  44441  ntrneikb  44539  elnev  44882  onfrALTlem5  44987  onfrALTlem5VD  45329  ndisj2  45500  ndmaovcom  47665  usgrexmpl2nb3  48522  eliunxp2  48822  mpomptx2  48823  mo0sn  49303  i0oii  49407  io1ii  49408  alimp-no-surprise  50268  alsi-no-surprise  50283