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  1521  sbrimvw  2091  2eu4  2655  2eu5  2656  r19.41v  3189  r3ex  3198  r19.41  3263  sbralie  3358  pm13.183  3666  euxfrw  3727  euxfr  3729  euind  3730  rmo4  3736  rmo3f  3740  2reu5lem3  3763  rmo3  3889  difin  4272  indifdi  4294  ab0orv  4383  dftr5  5263  axsepgfromrep  5294  inuni  5350  reusv2lem4  5401  rabxp  5733  elvvv  5761  eliunxp  5848  elidinxp  6062  imadisj  6098  idrefALT  6131  intirr  6138  resco  6270  funcnv3  6636  fncnv  6639  fun11  6640  fununi  6641  mptfnf  6703  f1mpt  7281  mpomptx  7546  uniuni  7782  frxp  8151  xpord2pred  8170  xpord2indlem  8172  oeeu  8641  ixp0x  8966  xpcomco  9102  1sdomOLD  9285  dffi3  9471  wemapsolem  9590  cardval3  9992  kmlem4  10194  kmlem12  10202  kmlem14  10204  kmlem15  10205  kmlem16  10206  fpwwe2  10683  axgroth4  10872  ltexprlem4  11079  bitsmod  16473  pythagtrip  16872  isstruct  17189  pgpfac1  20100  pgpfac  20104  basdif0  22960  ntreq0  23085  tgcmp  23409  tx1cn  23617  rnelfmlem  23960  phtpcer  25027  iscvsp  25161  caucfil  25317  minveclem1  25458  ovoliunlem1  25537  mdegleb  26103  eqscut2  27851  dmscut  27856  made0  27912  mulsuniflem  28175  istrkg2ld  28468  numedglnl  29161  usgr2pth0  29785  adjbd1o  32104  nmo  32509  dmrab  32516  difrab2  32517  mpomptxf  32687  ccfldextdgrr  33722  fldextrspunlsplem  33723  isros  34169  1stmbfm  34262  bnj976  34791  bnj1143  34804  bnj1533  34866  bnj864  34936  bnj983  34965  bnj1174  35017  bnj1175  35018  bnj1280  35034  cvmlift2lem12  35319  axacprim  35707  dfrecs2  35951  andnand1  36402  bj-snglc  36970  bj-disj2r  37029  bj-dfmpoa  37119  bj-mpomptALT  37120  mptsnunlem  37339  wl-df3xor2  37470  wl-df4-3mintru2  37488  wl-cases2-dnf  37513  wl-euae  37518  itg2addnc  37681  asindmre  37710  brres2  38269  brxrn2  38376  dfxrn2  38377  inxpxrn  38396  refsymrel2  38568  refsymrel3  38569  dfeqvrel2  38591  dfeqvrel3  38592  isopos  39181  dihglblem6  41342  dihglb2  41344  fgraphopab  43215  unielss  43230  dflim5  43342  ifpid2g  43506  ifpim23g  43508  rp-fakeanorass  43526  en2pr  43560  elmapintrab  43589  relnonrel  43600  undmrnresiss  43617  elintima  43666  relexp0eq  43714  iunrelexp0  43715  dffrege115  43991  frege131  44007  frege133  44009  ntrneikb  44107  elnev  44457  onfrALTlem5  44562  onfrALTlem5VD  44905  ndisj2  45056  ndmaovcom  47217  usgrexmpl2nb3  47993  eliunxp2  48250  mpomptx2  48251  mo0sn  48735  i0oii  48817  io1ii  48818  alimp-no-surprise  49300  alsi-no-surprise  49315