![]() |
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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: inimasn 4892 dmfco 5421 omp1eomlem 6894 ltanqg 7109 genpassl 7233 genpassu 7234 ltexprlemloc 7316 caucvgprlemcanl 7353 cauappcvgprlemladdrl 7366 caucvgprlemladdrl 7387 caucvgprprlemaddq 7417 apneg 8239 lemuldiv 8497 msq11 8518 negiso 8571 avglt2 8811 xleaddadd 9511 iooshf 9576 qtri3or 9861 sq11ap 10299 hashen 10371 fihashdom 10390 cjap 10519 sqrt11ap 10650 xrnegiso 10870 clim2c 10892 climabs0 10915 absefib 11274 efieq1re 11275 nndivides 11295 oddnn02np1 11372 oddge22np1 11373 evennn02n 11374 evennn2n 11375 halfleoddlt 11386 cnntr 12175 cndis 12191 cnpdis 12192 lmres 12198 blininf 12352 cncfmet 12492 |
Copyright terms: Public domain | W3C validator |