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  2849  frecsuclem  6671  mapsnend  7093  indpi  7703  cauappcvgprlemladdru  8017  prsrlt  8148  lesub2  8779  ltsub2  8781  rec11ap  9034  avglt1  9527  rpnegap  10070  modqmuladdnn0  10788  expap0  10989  hashf1lem1  11268  swrdspsleq  11422  2shfti  11579  mulreap  11612  minmax  11979  lemininf  11983  xrminmax  12014  xrlemininf  12020  modremain  12679  nnwosdc  12799  nn0seqcvgd  12802  divgcdcoprm0  12862  ballotfilemsima  13242  ismgmid  13680  grpsubeq0  13874  grpsubadd  13876  eqg0el  14015  isunitd  14396  lsslss  14701  isridlrng  14802  zndvds  14967  znleval  14971  isxmet2d  15432  xblss2  15489  neibl  15575  ellimc3apf  15744  logbgt0b  16051  lgsne0  16140  lgsabs1  16141  lgsquadlem1  16179  m1lgs  16187  eupth2lem2dc  16683  eupth2lem3lem4fi  16697  iswomninnlem  17073