Theorem 3bitr4ri 213

Description: A chained inference from transitive law for logical equivalence. (Contributed by NM, 2-Sep-1995.)

Hypotheses

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

Assertion

Ref	Expression
3bitr4ri	|- ( th <-> ch )

Proof of Theorem 3bitr4ri

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

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  dcnnOLD  850  excxor  1397  sbequ8  1869  2sb5  2010  2sb6  2011  2sb5rf  2016  2sb6rf  2017  moabs  2102  moanim  2127  2eu4  2146  2eu7  2147  sb8ab  2326  risset  2533  cbvreuvw  2743  reuind  2977  difundi  3424  indifdir  3428  unab  3439  inab  3440  rabeq0  3489  abeq0  3490  inssdif0im  3527  snprc  3697  snssOLD  3758  unipr  3863  uni0b  3874  pwtr  4262  opm  4277  onintexmid  4620  elxp2  4692  opthprc  4725  xpiundir  4733  elvvv  4737  relun  4791  inopab  4809  difopab  4810  ralxpf  4823  rexxpf  4824  dmiun  4886  rniun  5092  cnvresima  5171  imaco  5187  fnopabg  5398  dff1o2  5526  idref  5824  imaiun  5828  opabex3d  6205  opabex3  6206  onntri35  7348  elixx3g  10022  elfz2  10136  elfzuzb  10140  divalgb  12207  1nprm  12407  issubg3  13499  cnfldui  14322  alsconv  15981