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  1361  2eu4  2375  2eu5  2377  exists1  2383  euxfr  3244  euind  3245  rmo4  3251  2reu5lem3  3266  rmo3  3385  difin  3687  difin0ss  3845  reusv2lem4  4596  reusv6OLD  4603  reusv7OLD  4604  rabxp  4975  eliunxp  5077  imadisj  5288  intirr  5316  resco  5442  funcnv3  5579  fncnv  5582  fun11  5583  fununi  5584  f1mpt  6075  mpt2mptx  6283  uniuni  6487  frxp  6784  oeeu  7144  ixp0x  7393  mapsnen  7489  xpcomco  7503  1sdom  7618  dffi3  7784  cardval3  8225  kmlem4  8425  kmlem12  8433  kmlem14  8435  kmlem15  8436  kmlem16  8437  fpwwe2  8913  axgroth4  9102  ltexprlem4  9311  bitsmod  13736  pythagtrip  14005  pgpfac1  16688  pgpfac  16692  isassa  17495  istps3OLD  18645  basdif0  18676  ntreq0  18799  tgcmp  19122  tx1cn  19300  rnelfmlem  19643  phtpcer  20685  caucfil  20912  minveclem1  21029  ovoliunlem1  21103  mdegleb  21653  istrkg2ld  23040  3v3e3cycl2  23687  adjbd1o  25626  nmo  26006  rmo3f  26016  rmo4fOLD  26017  mptfnf  26112  mpt2mptxf  26131  1stmbfm  26811  cvmlift2lem12  27339  axacprim  27494  andnand1  28381  itg2addnc  28586  asindmre  28619  fgraphopab  29718  ndmaovcom  30251  usgra2pth0  30442  iswwlk  30457  eliunxp2  30861  mpt2mptx2  30864  alimp-no-surprise  31435  alsi-no-surprise  31450  onfrALTlem5  31552  bnj976  32073  bnj1143  32086  bnj1533  32147  bnj864  32217  bnj983  32246  bnj1174  32296  bnj1175  32297  bnj1280  32313  bj-denotes  32671  bj-snglc  32764  isopos  33133  dihglblem6  35293  dihglb2  35295