![]() |
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 4964 dmfco 5497 omp1eomlem 6987 ltanqg 7232 genpassl 7356 genpassu 7357 ltexprlemloc 7439 caucvgprlemcanl 7476 cauappcvgprlemladdrl 7489 caucvgprlemladdrl 7510 caucvgprprlemaddq 7540 apneg 8397 lemuldiv 8663 msq11 8684 negiso 8737 avglt2 8983 xleaddadd 9700 iooshf 9765 qtri3or 10051 sq11ap 10489 hashen 10562 fihashdom 10581 cjap 10710 sqrt11ap 10842 xrnegiso 11063 clim2c 11085 climabs0 11108 absefib 11513 efieq1re 11514 nndivides 11536 oddnn02np1 11613 oddge22np1 11614 evennn02n 11615 evennn2n 11616 halfleoddlt 11627 cnntr 12433 cndis 12449 cnpdis 12450 lmres 12456 txhmeo 12527 blininf 12632 cncfmet 12787 |
Copyright terms: Public domain | W3C validator |