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  854  excxor  1420  sbequ8  1893  2sb5  2034  2sb6  2035  2sb5rf  2040  2sb6rf  2041  moabs  2127  moanim  2152  2eu4  2171  2eu7  2172  sb8ab  2351  risset  2558  cbvreuvw  2771  reuind  3009  difundi  3457  indifdir  3461  unab  3472  inab  3473  rabeq0  3522  abeq0  3523  inssdif0im  3560  snprc  3732  snssOLD  3797  unipr  3905  uni0b  3916  pwtr  4309  opm  4324  onintexmid  4669  elxp2  4741  opthprc  4775  xpiundir  4783  elvvv  4787  relun  4842  inopab  4860  difopab  4861  ralxpf  4874  rexxpf  4875  dmiun  4938  rniun  5145  cnvresima  5224  imaco  5240  fnopabg  5453  dff1o2  5585  idref  5892  imaiun  5896  opabex3d  6278  opabex3  6279  onntri35  7445  elixx3g  10126  elfz2  10240  elfzuzb  10244  divalgb  12476  1nprm  12676  issubg3  13769  cnfldui  14593  alsconv  16620