Theorem 3bitr2d 216

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

Hypotheses

Ref	Expression
3bitr2d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr2d.2	⊢ (𝜑 → (𝜃 ↔ 𝜒))
3bitr2d.3	⊢ (𝜑 → (𝜃 ↔ 𝜏))

Assertion

Ref	Expression
3bitr2d	⊢ (𝜑 → (𝜓 ↔ 𝜏))

Proof of Theorem 3bitr2d

Step	Hyp	Ref	Expression
1		3bitr2d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2		3bitr2d.2	. . 3 ⊢ (𝜑 → (𝜃 ↔ 𝜒))
3	1, 2	bitr4d 191	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃))
4		3bitr2d.3	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏))
5	3, 4	bitrd 188	1 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ 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:  ceqsralt  2829  frecsuclem  6577  indpi  7567  cauappcvgprlemladdru  7881  prsrlt  8012  lesub2  8642  ltsub2  8644  rec11ap  8895  avglt1  9388  rpnegap  9926  modqmuladdnn0  10636  expap0  10837  swrdspsleq  11257  2shfti  11414  mulreap  11447  minmax  11813  lemininf  11817  xrminmax  11848  xrlemininf  11854  modremain  12513  nnwosdc  12633  nn0seqcvgd  12636  divgcdcoprm0  12696  ismgmid  13483  grpsubeq0  13692  grpsubadd  13694  eqg0el  13839  isunitd  14144  lsslss  14419  isridlrng  14520  zndvds  14687  znleval  14691  isxmet2d  15101  xblss2  15158  neibl  15244  ellimc3apf  15413  logbgt0b  15719  lgsne0  15796  lgsabs1  15797  lgsquadlem1  15835  m1lgs  15843  eupth2lem2dc  16339  eupth2lem3lem4fi  16353  iswomninnlem  16721