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  2840  frecsuclem  6636  mapsnend  7051  indpi  7653  cauappcvgprlemladdru  7967  prsrlt  8098  lesub2  8727  ltsub2  8729  rec11ap  8980  avglt1  9473  rpnegap  10015  modqmuladdnn0  10726  expap0  10927  swrdspsleq  11352  2shfti  11509  mulreap  11542  minmax  11908  lemininf  11912  xrminmax  11943  xrlemininf  11949  modremain  12608  nnwosdc  12728  nn0seqcvgd  12731  divgcdcoprm0  12791  ismgmid  13579  grpsubeq0  13788  grpsubadd  13790  eqg0el  13935  isunitd  14240  lsslss  14516  isridlrng  14617  zndvds  14784  znleval  14788  isxmet2d  15200  xblss2  15257  neibl  15343  ellimc3apf  15512  logbgt0b  15818  lgsne0  15898  lgsabs1  15899  lgsquadlem1  15937  m1lgs  15945  eupth2lem2dc  16441  eupth2lem3lem4fi  16455  iswomninnlem  16821