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  1522  sbrimvw  2096  2eu4  2655  2eu5  2656  r19.41v  3166  r3ex  3175  r19.41  3240  sbralie  3322  sbralieOLD  3324  pm13.183  3620  euxfrw  3679  euxfr  3681  euind  3682  rmo4  3688  rmo3f  3692  2reu5lem3  3715  rmo3  3839  difin  4224  indifdi  4246  dftr5  5209  axsepgfromrep  5239  inuni  5295  reusv2lem4  5346  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  7207  mpomptx  7471  uniuni  7707  frxp  8068  xpord2pred  8087  xpord2indlem  8089  oeeu  8531  ixp0x  8864  xpcomco  8995  dffi3  9334  wemapsolem  9455  cardval3  9864  kmlem4  10064  kmlem12  10072  kmlem14  10074  kmlem15  10075  kmlem16  10076  fpwwe2  10554  axgroth4  10743  ltexprlem4  10950  bitsmod  16363  pythagtrip  16762  isstruct  17079  pgpfac1  20011  pgpfac  20015  basdif0  22897  ntreq0  23021  tgcmp  23345  tx1cn  23553  rnelfmlem  23896  phtpcer  24950  iscvsp  25084  caucfil  25239  minveclem1  25380  ovoliunlem1  25459  mdegleb  26025  eqcuts2  27782  dmcuts  27787  made0  27859  mulsuniflem  28145  istrkg2ld  28532  numedglnl  29217  usgr2pth0  29838  adjbd1o  32160  nmo  32564  dmrab  32571  difrab2  32572  mpomptxf  32757  ccfldextdgrr  33829  fldextrspunlsplem  33830  isros  34325  1stmbfm  34417  bnj976  34933  bnj1143  34946  bnj1533  35008  bnj864  35078  bnj983  35107  bnj1174  35159  bnj1175  35160  bnj1280  35176  axregs  35295  onvf1odlem2  35298  cvmlift2lem12  35508  axacprim  35901  dfrecs2  36144  andnand1  36595  bj-snglc  37170  bj-disj2r  37229  bj-dfmpoa  37323  bj-mpomptALT  37324  mptsnunlem  37543  wl-df3xor2  37674  wl-df4-3mintru2  37692  wl-cases2-dnf  37717  wl-euae  37722  itg2addnc  37875  asindmre  37904  brres2  38466  brxrn2  38569  dfxrn2  38570  inxpxrn  38603  dfsuccl4  38648  refsymrel2  38824  refsymrel3  38825  dfeqvrel2  38847  dfeqvrel3  38848  isopos  39440  dihglblem6  41600  dihglb2  41602  fgraphopab  43445  unielss  43460  dflim5  43571  ifpid2g  43734  ifpim23g  43736  rp-fakeanorass  43754  en2pr  43788  elmapintrab  43817  relnonrel  43828  undmrnresiss  43845  elintima  43894  relexp0eq  43942  iunrelexp0  43943  dffrege115  44219  frege131  44235  frege133  44237  ntrneikb  44335  elnev  44678  onfrALTlem5  44783  onfrALTlem5VD  45125  ndisj2  45296  ndmaovcom  47451  usgrexmpl2nb3  48280  eliunxp2  48580  mpomptx2  48581  mo0sn  49061  i0oii  49165  io1ii  49166  alimp-no-surprise  50026  alsi-no-surprise  50041