Theorem 3bitr4rd 221

Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)

Hypotheses

Ref	Expression
3bitr4d.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))
3bitr4d.2	⊢ (𝜑 → (𝜃 ↔ 𝜓))
3bitr4d.3	⊢ (𝜑 → (𝜏 ↔ 𝜒))

Assertion

Ref	Expression
3bitr4rd	⊢ (𝜑 → (𝜏 ↔ 𝜃))

Proof of Theorem 3bitr4rd

Step	Hyp	Ref	Expression
1		3bitr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
2		3bitr4d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	bitr4d 191	. 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓))
4		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
5	3, 4	bitr4d 191	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:  inimasn  5154  dmfco  5714  omp1eomlem  7293  ltanqg  7620  genpassl  7744  genpassu  7745  ltexprlemloc  7827  caucvgprlemcanl  7864  cauappcvgprlemladdrl  7877  caucvgprlemladdrl  7898  caucvgprprlemaddq  7928  apneg  8791  lemuldiv  9061  msq11  9082  negiso  9135  avglt2  9384  xleaddadd  10122  iooshf  10187  qtri3or  10501  sq11ap  10970  hashen  11047  fihashdom  11067  cjap  11484  sqrt11ap  11616  mingeb  11820  xrnegiso  11840  clim2c  11862  climabs0  11885  absefib  12350  efieq1re  12351  nndivides  12376  oddnn02np1  12459  oddge22np1  12460  evennn02n  12461  evennn2n  12462  halfleoddlt  12473  pc2dvds  12921  pcmpt  12934  issubm  13573  cnntr  14968  cndis  14984  cnpdis  14985  lmres  14991  txhmeo  15062  blininf  15167  cncfmet  15335