Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitr4rd | GIF version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.) |
Ref | Expression |
---|---|
3bitr4d.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitr4d.2 | ⊢ (𝜑 → (𝜃 ↔ 𝜓)) |
3bitr4d.3 | ⊢ (𝜑 → (𝜏 ↔ 𝜒)) |
Ref | Expression |
---|---|
3bitr4rd | ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitr4d.3 | . . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒)) | |
2 | 3bitr4d.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
3 | 1, 2 | bitr4d 190 | . 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
4 | 3bitr4d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | |
5 | 3, 4 | bitr4d 190 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: inimasn 5028 dmfco 5564 omp1eomlem 7071 ltanqg 7362 genpassl 7486 genpassu 7487 ltexprlemloc 7569 caucvgprlemcanl 7606 cauappcvgprlemladdrl 7619 caucvgprlemladdrl 7640 caucvgprprlemaddq 7670 apneg 8530 lemuldiv 8797 msq11 8818 negiso 8871 avglt2 9117 xleaddadd 9844 iooshf 9909 qtri3or 10199 sq11ap 10643 hashen 10718 fihashdom 10738 cjap 10870 sqrt11ap 11002 mingeb 11205 xrnegiso 11225 clim2c 11247 climabs0 11270 absefib 11733 efieq1re 11734 nndivides 11759 oddnn02np1 11839 oddge22np1 11840 evennn02n 11841 evennn2n 11842 halfleoddlt 11853 pc2dvds 12283 pcmpt 12295 issubm 12695 cnntr 13019 cndis 13035 cnpdis 13036 lmres 13042 txhmeo 13113 blininf 13218 cncfmet 13373 |
Copyright terms: Public domain | W3C validator |