Theorem 3bitr4ri 212

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 186	. 2 |- ( ph <-> th )
5	1, 4	bitr2i 184	1 |- ( th <-> ch )

Syntax hints:   <-> wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  dcnnOLD  834  excxor  1356  sbequ8  1819  2sb5  1958  2sb6  1959  2sb5rf  1964  2sb6rf  1965  moabs  2048  moanim  2073  2eu4  2092  2eu7  2093  sb8ab  2261  risset  2463  reuind  2889  difundi  3328  indifdir  3332  unab  3343  inab  3344  rabeq0  3392  abeq0  3393  inssdif0im  3430  snprc  3588  snss  3649  unipr  3750  uni0b  3761  pwtr  4141  opm  4156  onintexmid  4487  elxp2  4557  opthprc  4590  xpiundir  4598  elvvv  4602  relun  4656  inopab  4671  difopab  4672  ralxpf  4685  rexxpf  4686  dmiun  4748  rniun  4949  cnvresima  5028  imaco  5044  fnopabg  5246  dff1o2  5372  idref  5658  imaiun  5661  opabex3d  6019  opabex3  6020  elixx3g  9684  elfz2  9797  elfzuzb  9800  divalgb  11622  1nprm  11795  alsconv  13246