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  5048  dmfco  5587  omp1eomlem  7096  ltanqg  7402  genpassl  7526  genpassu  7527  ltexprlemloc  7609  caucvgprlemcanl  7646  cauappcvgprlemladdrl  7659  caucvgprlemladdrl  7680  caucvgprprlemaddq  7710  apneg  8571  lemuldiv  8841  msq11  8862  negiso  8915  avglt2  9161  xleaddadd  9890  iooshf  9955  qtri3or  10246  sq11ap  10691  hashen  10767  fihashdom  10786  cjap  10918  sqrt11ap  11050  mingeb  11253  xrnegiso  11273  clim2c  11295  climabs0  11318  absefib  11781  efieq1re  11782  nndivides  11807  oddnn02np1  11888  oddge22np1  11889  evennn02n  11890  evennn2n  11891  halfleoddlt  11902  pc2dvds  12332  pcmpt  12344  issubm  12870  cnntr  13886  cndis  13902  cnpdis  13903  lmres  13909  txhmeo  13980  blininf  14085  cncfmet  14240