Theorem 3bitr2i 273

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 252	. 2 |- ( ph <-> ch )
4		3bitr2i.3	. 2 |- ( ch <-> th )
5	3, 4	bitri 249	1 |- ( ph <-> th )

Syntax hints:   <-> wb 184

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 185

This theorem is referenced by:  con2bi  326  an13  797  xorneg2  1373  xorneg1OLD  1375  2eu4  2311  2eu5  2313  exists1  2319  euxfr  3210  euind  3211  rmo4  3217  2reu5lem3  3232  rmo3  3343  difin  3660  difin0ss  3810  reusv2lem4  4569  rabxp  4950  eliunxp  5053  imadisj  5268  intirr  5298  resco  5419  funcnv3  5557  fncnv  5560  fun11  5561  fununi  5562  f1mpt  6070  mpt2mptx  6292  uniuni  6508  frxp  6809  oeeu  7170  ixp0x  7416  mapsnen  7512  xpcomco  7526  1sdom  7639  dffi3  7806  wemapsolem  7890  cardval3  8246  kmlem4  8446  kmlem12  8454  kmlem14  8456  kmlem15  8457  kmlem16  8458  fpwwe2  8932  axgroth4  9121  ltexprlem4  9328  bitsmod  14088  pythagtrip  14360  pgpfac1  17244  pgpfac  17248  isassa  18077  istps3OLD  19508  basdif0  19539  ntreq0  19664  tgcmp  19987  tx1cn  20195  rnelfmlem  20538  phtpcer  21580  caucfil  21807  minveclem1  21924  ovoliunlem1  21998  mdegleb  22549  istrkg2ld  23975  3v3e3cycl2  24785  iswwlk  24804  adjbd1o  27120  nmo  27501  rmo3f  27511  rmo4fOLD  27512  mptfnf  27640  mpt2mptxf  27665  1stmbfm  28387  cvmlift2lem12  28948  axacprim  29245  andnand1  30017  wl-cases2-dnf  30135  itg2addnc  30235  asindmre  30268  fgraphopab  31338  ndmaovcom  32456  usgra2pth0  32673  eliunxp2  33123  mpt2mptx2  33124  alimp-no-surprise  33530  alsi-no-surprise  33545  onfrALTlem5  33654  bnj976  34183  bnj1143  34196  bnj1533  34257  bnj864  34327  bnj983  34356  bnj1174  34406  bnj1175  34407  bnj1280  34423  bj-denotes  34781  bj-snglc  34875  isopos  35318  dihglblem6  37480  dihglb2  37482  ifpid2g  38123  ifpim23g  38128  rp-fakeanorass  38167  elintima  38195  relexp0eq  38236  iunrelexp0  38242  dffrege115  38477  frege131  38493  frege133  38495