Theorem 3bitr2d 216

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

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

Assertion

Ref	Expression
3bitr2d	|- ( ph -> ( ps <-> ta ) )

Proof of Theorem 3bitr2d

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
2		3bitr2d.2	. . 3 |- ( ph -> ( th <-> ch ) )
3	1, 2	bitr4d 191	. 2 |- ( ph -> ( ps <-> th ) )
4		3bitr2d.3	. 2 |- ( ph -> ( th <-> ta ) )
5	3, 4	bitrd 188	1 |- ( ph -> ( ps <-> ta ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ceqsralt  2849  frecsuclem  6677  mapsnend  7099  indpi  7710  cauappcvgprlemladdru  8024  prsrlt  8155  lesub2  8787  ltsub2  8789  rec11ap  9043  avglt1  9549  rpnegap  10098  modqmuladdnn0  10820  expap0  11021  hashf1lem1  11301  swrdspsleq  11455  2shfti  11612  mulreap  11645  minmax  12014  lemininf  12018  xrminmax  12050  xrlemininf  12056  modremain  12715  nnwosdc  12835  nn0seqcvgd  12838  divgcdcoprm0  12898  ballotfilemsima  13311  ismgmid  13750  grpsubeq0  13944  grpsubadd  13946  eqg0el  14085  isunitd  14497  lsslss  14802  isridlrng  14903  zndvds  15068  znleval  15072  isxmet2d  15540  xblss2  15597  neibl  15683  ellimc3apf  15852  logbgt0b  16163  prmefexple  16269  bposlem7  16278  lgsne0  16323  lgsabs1  16324  lgsquadlem1  16362  m1lgs  16370  eupth2lem2dc  16866  eupth2lem3lem4fi  16880  iswomninnlem  17266