Theorem 3bitr2i 281

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

Syntax hints:   <-> wb 189

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 190

This theorem is referenced by:  con2bi  334  an13  813  xorneg2  1426  xorneg1OLD  1428  2eu4  2396  2eu5  2397  exists1  2401  euxfr  3236  euind  3237  rmo4  3243  2reu5lem3  3259  rmo3  3370  difin  3692  difin0ss  3845  reusv2lem4  4621  rabxp  4890  eliunxp  4991  imadisj  5206  intirr  5237  resco  5358  funcnv3  5666  fncnv  5669  fun11  5670  fununi  5671  mptfnf  5721  f1mpt  6187  mpt2mptx  6414  uniuni  6627  frxp  6933  oeeu  7330  ixp0x  7576  mapsnen  7673  xpcomco  7688  1sdom  7801  dffi3  7971  wemapsolem  8091  cardval3  8412  kmlem4  8609  kmlem12  8617  kmlem14  8619  kmlem15  8620  kmlem16  8621  fpwwe2  9094  axgroth4  9283  ltexprlem4  9490  bitsmod  14459  pythagtrip  14833  pgpfac1  17762  pgpfac  17766  isassa  18588  basdif0  20017  ntreq0  20142  tgcmp  20465  tx1cn  20673  rnelfmlem  21016  phtpcer  22075  caucfil  22302  minveclem1  22415  ovoliunlem1  22504  mdegleb  23062  istrkg2ld  24557  3v3e3cycl2  25441  iswwlk  25460  adjbd1o  27787  nmo  28170  rmo3f  28180  rmo4fOLD  28181  mpt2mptxf  28329  isros  29039  1stmbfm  29131  bnj976  29638  bnj1143  29651  bnj1533  29712  bnj864  29782  bnj983  29811  bnj1174  29861  bnj1175  29862  bnj1280  29878  cvmlift2lem12  30086  axacprim  30383  dfrecs2  30766  andnand1  31108  bj-dfssb2  31298  bj-denotes  31512  bj-snglc  31608  bj-dfmpt2a  31675  bj-mpt2mptALT  31676  mptsnunlem  31785  wl-cases2-dnf  31895  itg2addnc  32041  asindmre  32072  isopos  32791  dihglblem6  34953  dihglb2  34955  fgraphopab  36132  ifpid2g  36182  ifpim23g  36184  rp-fakeanorass  36202  elmapintrab  36227  relintabex  36232  relnonrel  36238  undmrnresiss  36255  elintima  36290  relexp0eq  36338  iunrelexp0  36339  dffrege115  36619  frege131  36635  frege133  36637  onfrALTlem5  36952  ndisj2  37427  ndmaovcom  38745  usgra2pth0  39942  eliunxp2  40388  mpt2mptx2  40389  alimp-no-surprise  40793  alsi-no-surprise  40808