Theorem 3bitr2i 277

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr2i.1	|- ( ph <-> ps )
3bitr2i.2	|- ( ch <-> ps )
3bitr2i.3	|- ( ch <-> th )

Assertion

Ref	Expression
3bitr2i	|- ( ph <-> th )

Proof of Theorem 3bitr2i

Step	Hyp	Ref	Expression
1		3bitr2i.1	. . 3 |- ( ph <-> ps )
2		3bitr2i.2	. . 3 |- ( ch <-> ps )
3	1, 2	bitr4i 256	. 2 |- ( ph <-> ch )
4		3bitr2i.3	. 2 |- ( ch <-> th )
5	3, 4	bitri 253	1 |- ( ph <-> th )

Syntax hints:   <-> wb 188

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 189

This theorem is referenced by:  con2bi  330  an13  807  xorneg2  1412  xorneg1OLD  1414  2eu4  2355  2eu5  2356  exists1  2360  euxfr  3258  euind  3259  rmo4  3265  2reu5lem3  3281  rmo3  3392  difin  3712  difin0ss  3863  reusv2lem4  4627  rabxp  4889  eliunxp  4990  imadisj  5205  intirr  5236  resco  5357  funcnv3  5661  fncnv  5664  fun11  5665  fununi  5666  mptfnf  5716  f1mpt  6176  mpt2mptx  6400  uniuni  6613  frxp  6916  oeeu  7314  ixp0x  7560  mapsnen  7656  xpcomco  7670  1sdom  7783  dffi3  7953  wemapsolem  8073  cardval3  8393  kmlem4  8589  kmlem12  8597  kmlem14  8599  kmlem15  8600  kmlem16  8601  fpwwe2  9074  axgroth4  9263  ltexprlem4  9470  bitsmod  14407  pythagtrip  14781  pgpfac1  17710  pgpfac  17714  isassa  18536  basdif0  19964  ntreq0  20089  tgcmp  20412  tx1cn  20620  rnelfmlem  20963  phtpcer  22022  caucfil  22249  minveclem1  22362  ovoliunlem1  22451  mdegleb  23009  istrkg2ld  24504  3v3e3cycl2  25388  iswwlk  25407  adjbd1o  27734  nmo  28117  rmo3f  28127  rmo4fOLD  28128  mpt2mptxf  28280  isros  28996  1stmbfm  29088  bnj976  29595  bnj1143  29608  bnj1533  29669  bnj864  29739  bnj983  29768  bnj1174  29818  bnj1175  29819  bnj1280  29835  cvmlift2lem12  30043  axacprim  30340  dfrecs2  30720  andnand1  31062  bj-denotes  31435  bj-snglc  31529  mptsnunlem  31702  wl-cases2-dnf  31812  itg2addnc  31958  asindmre  31989  isopos  32713  dihglblem6  34875  dihglb2  34877  fgraphopab  36055  ifpid2g  36105  ifpim23g  36107  rp-fakeanorass  36125  elintima  36153  relexp0eq  36201  iunrelexp0  36202  dffrege115  36480  frege131  36496  frege133  36498  onfrALTlem5  36814  ndisj2  37299  ndmaovcom  38467  usgra2pth0  39061  eliunxp2  39509  mpt2mptx2  39510  alimp-no-surprise  39914  alsi-no-surprise  39929