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  6650  mapsnend  7065  indpi  7673  cauappcvgprlemladdru  7987  prsrlt  8118  lesub2  8749  ltsub2  8751  rec11ap  9004  avglt1  9497  rpnegap  10040  modqmuladdnn0  10757  expap0  10958  swrdspsleq  11387  2shfti  11544  mulreap  11577  minmax  11943  lemininf  11947  xrminmax  11978  xrlemininf  11984  modremain  12643  nnwosdc  12763  nn0seqcvgd  12766  divgcdcoprm0  12826  ballotfilemsima  13206  ismgmid  13643  grpsubeq0  13844  grpsubadd  13846  eqg0el  13985  isunitd  14354  lsslss  14658  isridlrng  14759  zndvds  14926  znleval  14930  isxmet2d  15342  xblss2  15399  neibl  15485  ellimc3apf  15654  logbgt0b  15960  lgsne0  16040  lgsabs1  16041  lgsquadlem1  16079  m1lgs  16087  eupth2lem2dc  16583  eupth2lem3lem4fi  16597  iswomninnlem  16973