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  2800  frecsuclem  6499  indpi  7462  cauappcvgprlemladdru  7776  prsrlt  7907  lesub2  8537  ltsub2  8539  rec11ap  8790  avglt1  9283  rpnegap  9815  modqmuladdnn0  10520  expap0  10721  swrdspsleq  11128  2shfti  11186  mulreap  11219  minmax  11585  lemininf  11589  xrminmax  11620  xrlemininf  11626  modremain  12284  nnwosdc  12404  nn0seqcvgd  12407  divgcdcoprm0  12467  ismgmid  13253  grpsubeq0  13462  grpsubadd  13464  eqg0el  13609  isunitd  13912  lsslss  14187  isridlrng  14288  zndvds  14455  znleval  14459  isxmet2d  14864  xblss2  14921  neibl  15007  ellimc3apf  15176  logbgt0b  15482  lgsne0  15559  lgsabs1  15560  lgsquadlem1  15598  m1lgs  15606  iswomninnlem  16062