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  2807  frecsuclem  6522  indpi  7497  cauappcvgprlemladdru  7811  prsrlt  7942  lesub2  8572  ltsub2  8574  rec11ap  8825  avglt1  9318  rpnegap  9850  modqmuladdnn0  10557  expap0  10758  swrdspsleq  11165  2shfti  11308  mulreap  11341  minmax  11707  lemininf  11711  xrminmax  11742  xrlemininf  11748  modremain  12406  nnwosdc  12526  nn0seqcvgd  12529  divgcdcoprm0  12589  ismgmid  13376  grpsubeq0  13585  grpsubadd  13587  eqg0el  13732  isunitd  14035  lsslss  14310  isridlrng  14411  zndvds  14578  znleval  14582  isxmet2d  14987  xblss2  15044  neibl  15130  ellimc3apf  15299  logbgt0b  15605  lgsne0  15682  lgsabs1  15683  lgsquadlem1  15721  m1lgs  15729  iswomninnlem  16328