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 ⊢ (𝜑 → (𝜓 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ceqsralt  2849  frecsuclem  6681  mapsnend  7104  indpi  7716  cauappcvgprlemladdru  8030  prsrlt  8161  lesub2  8793  ltsub2  8795  rec11ap  9049  avglt1  9556  rpnegap  10105  modqmuladdnn0  10827  expap0  11028  hashf1lem1  11308  swrdspsleq  11462  2shfti  11619  mulreap  11652  minmax  12021  lemininf  12025  xrminmax  12057  xrlemininf  12063  modremain  12722  nnwosdc  12842  nn0seqcvgd  12845  divgcdcoprm0  12905  ballotfilemsima  13318  ismgmid  13757  grpsubeq0  13951  grpsubadd  13953  eqg0el  14092  isunitd  14523  lsslss  14828  isridlrng  14929  zndvds  15094  znleval  15098  isxmet2d  15586  xblss2  15643  neibl  15729  ellimc3apf  15898  logbgt0b  16214  prmefexple  16320  bposlem7  16329  lgsne0  16374  lgsabs1  16375  lgsquadlem1  16413  m1lgs  16421  eupth2lem2dc  16917  eupth2lem3lem4fi  16931  iswomninnlem  17318