![]() |
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 191 | . 2 ⊢ (𝜑 → (𝜏 ↔ 𝜓)) |
4 | 3bitr4d.2 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓)) | |
5 | 3, 4 | bitr4d 191 | 1 ⊢ (𝜑 → (𝜏 ↔ 𝜃)) |
Colors of variables: wff set class |
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 5048 dmfco 5587 omp1eomlem 7096 ltanqg 7402 genpassl 7526 genpassu 7527 ltexprlemloc 7609 caucvgprlemcanl 7646 cauappcvgprlemladdrl 7659 caucvgprlemladdrl 7680 caucvgprprlemaddq 7710 apneg 8571 lemuldiv 8841 msq11 8862 negiso 8915 avglt2 9161 xleaddadd 9890 iooshf 9955 qtri3or 10246 sq11ap 10691 hashen 10767 fihashdom 10786 cjap 10918 sqrt11ap 11050 mingeb 11253 xrnegiso 11273 clim2c 11295 climabs0 11318 absefib 11781 efieq1re 11782 nndivides 11807 oddnn02np1 11888 oddge22np1 11889 evennn02n 11890 evennn2n 11891 halfleoddlt 11902 pc2dvds 12332 pcmpt 12344 issubm 12870 cnntr 13886 cndis 13902 cnpdis 13903 lmres 13909 txhmeo 13980 blininf 14085 cncfmet 14240 |
Copyright terms: Public domain | W3C validator |