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  2843  frecsuclem  6639  mapsnend  7054  indpi  7662  cauappcvgprlemladdru  7976  prsrlt  8107  lesub2  8736  ltsub2  8738  rec11ap  8989  avglt1  9482  rpnegap  10025  modqmuladdnn0  10737  expap0  10938  swrdspsleq  11367  2shfti  11524  mulreap  11557  minmax  11923  lemininf  11927  xrminmax  11958  xrlemininf  11964  modremain  12623  nnwosdc  12743  nn0seqcvgd  12746  divgcdcoprm0  12806  ismgmid  13611  grpsubeq0  13820  grpsubadd  13822  eqg0el  13967  isunitd  14273  lsslss  14578  isridlrng  14679  zndvds  14846  znleval  14850  isxmet2d  15262  xblss2  15319  neibl  15405  ellimc3apf  15574  logbgt0b  15880  lgsne0  15960  lgsabs1  15961  lgsquadlem1  15999  m1lgs  16007  eupth2lem2dc  16503  eupth2lem3lem4fi  16517  iswomninnlem  16883