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  6677  mapsnend  7099  indpi  7709  cauappcvgprlemladdru  8023  prsrlt  8154  lesub2  8785  ltsub2  8787  rec11ap  9041  avglt1  9546  rpnegap  10089  modqmuladdnn0  10807  expap0  11008  hashf1lem1  11287  swrdspsleq  11441  2shfti  11598  mulreap  11631  minmax  11998  lemininf  12002  xrminmax  12033  xrlemininf  12039  modremain  12698  nnwosdc  12818  nn0seqcvgd  12821  divgcdcoprm0  12881  ballotfilemsima  13261  ismgmid  13699  grpsubeq0  13893  grpsubadd  13895  eqg0el  14034  isunitd  14415  lsslss  14720  isridlrng  14821  zndvds  14986  znleval  14990  isxmet2d  15451  xblss2  15508  neibl  15594  ellimc3apf  15763  logbgt0b  16074  lgsne0  16169  lgsabs1  16170  lgsquadlem1  16208  m1lgs  16216  eupth2lem2dc  16712  eupth2lem3lem4fi  16726  iswomninnlem  17111