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  2827  frecsuclem  6558  indpi  7537  cauappcvgprlemladdru  7851  prsrlt  7982  lesub2  8612  ltsub2  8614  rec11ap  8865  avglt1  9358  rpnegap  9890  modqmuladdnn0  10598  expap0  10799  swrdspsleq  11207  2shfti  11350  mulreap  11383  minmax  11749  lemininf  11753  xrminmax  11784  xrlemininf  11790  modremain  12448  nnwosdc  12568  nn0seqcvgd  12571  divgcdcoprm0  12631  ismgmid  13418  grpsubeq0  13627  grpsubadd  13629  eqg0el  13774  isunitd  14078  lsslss  14353  isridlrng  14454  zndvds  14621  znleval  14625  isxmet2d  15030  xblss2  15087  neibl  15173  ellimc3apf  15342  logbgt0b  15648  lgsne0  15725  lgsabs1  15726  lgsquadlem1  15764  m1lgs  15772  iswomninnlem  16447