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  5146  dmfco  5704  omp1eomlem  7272  ltanqg  7598  genpassl  7722  genpassu  7723  ltexprlemloc  7805  caucvgprlemcanl  7842  cauappcvgprlemladdrl  7855  caucvgprlemladdrl  7876  caucvgprprlemaddq  7906  apneg  8769  lemuldiv  9039  msq11  9060  negiso  9113  avglt2  9362  xleaddadd  10095  iooshf  10160  qtri3or  10472  sq11ap  10941  hashen  11018  fihashdom  11037  cjap  11432  sqrt11ap  11564  mingeb  11768  xrnegiso  11788  clim2c  11810  climabs0  11833  absefib  12297  efieq1re  12298  nndivides  12323  oddnn02np1  12406  oddge22np1  12407  evennn02n  12408  evennn2n  12409  halfleoddlt  12420  pc2dvds  12868  pcmpt  12881  issubm  13520  cnntr  14914  cndis  14930  cnpdis  14931  lmres  14937  txhmeo  15008  blininf  15113  cncfmet  15281