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  5097  dmfco  5641  omp1eomlem  7178  ltanqg  7495  genpassl  7619  genpassu  7620  ltexprlemloc  7702  caucvgprlemcanl  7739  cauappcvgprlemladdrl  7752  caucvgprlemladdrl  7773  caucvgprprlemaddq  7803  apneg  8666  lemuldiv  8936  msq11  8957  negiso  9010  avglt2  9259  xleaddadd  9991  iooshf  10056  qtri3or  10364  sq11ap  10833  hashen  10910  fihashdom  10929  cjap  11136  sqrt11ap  11268  mingeb  11472  xrnegiso  11492  clim2c  11514  climabs0  11537  absefib  12001  efieq1re  12002  nndivides  12027  oddnn02np1  12110  oddge22np1  12111  evennn02n  12112  evennn2n  12113  halfleoddlt  12124  pc2dvds  12572  pcmpt  12585  issubm  13222  cnntr  14615  cndis  14631  cnpdis  14632  lmres  14638  txhmeo  14709  blininf  14814  cncfmet  14982