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  328  an13  797  xorneg1  1365  2eu4  2385  2eu5  2387  exists1  2393  euxfr  3284  euind  3285  rmo4  3291  2reu5lem3  3306  rmo3  3425  difin  3730  difin0ss  3888  reusv2lem4  4646  reusv6OLD  4653  reusv7OLD  4654  rabxp  5030  eliunxp  5133  imadisj  5349  intirr  5378  resco  5504  funcnv3  5642  fncnv  5645  fun11  5646  fununi  5647  f1mpt  6150  mpt2mptx  6370  uniuni  6582  frxp  6885  oeeu  7244  ixp0x  7489  mapsnen  7585  xpcomco  7599  1sdom  7714  dffi3  7882  cardval3  8324  kmlem4  8524  kmlem12  8532  kmlem14  8534  kmlem15  8535  kmlem16  8536  fpwwe2  9012  axgroth4  9201  ltexprlem4  9408  bitsmod  13936  pythagtrip  14208  pgpfac1  16916  pgpfac  16920  isassa  17730  istps3OLD  19185  basdif0  19216  ntreq0  19339  tgcmp  19662  tx1cn  19840  rnelfmlem  20183  phtpcer  21225  caucfil  21452  minveclem1  21569  ovoliunlem1  21643  mdegleb  22194  istrkg2ld  23581  3v3e3cycl2  24328  iswwlk  24347  adjbd1o  26668  nmo  27048  rmo3f  27058  rmo4fOLD  27059  mptfnf  27159  mpt2mptxf  27178  1stmbfm  27859  cvmlift2lem12  28387  axacprim  28542  andnand1  29429  itg2addnc  29635  asindmre  29668  fgraphopab  30766  ndmaovcom  31714  usgra2pth0  31781  eliunxp2  31864  mpt2mptx2  31865  alimp-no-surprise  32154  alsi-no-surprise  32169  onfrALTlem5  32271  bnj976  32792  bnj1143  32805  bnj1533  32866  bnj864  32936  bnj983  32965  bnj1174  33015  bnj1175  33016  bnj1280  33032  bj-denotes  33392  bj-snglc  33485  isopos  33854  dihglblem6  36014  dihglb2  36016