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 4951 dmfco 5482 omp1eomlem 6972 ltanqg 7201 genpassl 7325 genpassu 7326 ltexprlemloc 7408 caucvgprlemcanl 7445 cauappcvgprlemladdrl 7458 caucvgprlemladdrl 7479 caucvgprprlemaddq 7509 apneg 8366 lemuldiv 8632 msq11 8653 negiso 8706 avglt2 8952 xleaddadd 9663 iooshf 9728 qtri3or 10013 sq11ap 10451 hashen 10523 fihashdom 10542 cjap 10671 sqrt11ap 10803 xrnegiso 11024 clim2c 11046 climabs0 11069 absefib 11466 efieq1re 11467 nndivides 11489 oddnn02np1 11566 oddge22np1 11567 evennn02n 11568 evennn2n 11569 halfleoddlt 11580 cnntr 12383 cndis 12399 cnpdis 12400 lmres 12406 txhmeo 12477 blininf 12582 cncfmet 12737 |
Copyright terms: Public domain | W3C validator |