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  2828  frecsuclem  6565  indpi  7550  cauappcvgprlemladdru  7864  prsrlt  7995  lesub2  8625  ltsub2  8627  rec11ap  8878  avglt1  9371  rpnegap  9909  modqmuladdnn0  10618  expap0  10819  swrdspsleq  11235  2shfti  11379  mulreap  11412  minmax  11778  lemininf  11782  xrminmax  11813  xrlemininf  11819  modremain  12477  nnwosdc  12597  nn0seqcvgd  12600  divgcdcoprm0  12660  ismgmid  13447  grpsubeq0  13656  grpsubadd  13658  eqg0el  13803  isunitd  14107  lsslss  14382  isridlrng  14483  zndvds  14650  znleval  14654  isxmet2d  15059  xblss2  15116  neibl  15202  ellimc3apf  15371  logbgt0b  15677  lgsne0  15754  lgsabs1  15755  lgsquadlem1  15793  m1lgs  15801  iswomninnlem  16563