Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > 3bitrd | GIF version |
Description: Deduction from transitivity of biconditional. (Contributed by NM, 13-Aug-1999.) |
Ref | Expression |
---|---|
3bitrd.1 | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
3bitrd.2 | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
3bitrd.3 | ⊢ (𝜑 → (𝜃 ↔ 𝜏)) |
Ref | Expression |
---|---|
3bitrd | ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3bitrd.1 | . . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) | |
2 | 3bitrd.2 | . . 3 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) | |
3 | 1, 2 | bitrd 177 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3bitrd.3 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
5 | 3, 4 | bitrd 177 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: sbceqal 2814 sbcnel12g 2867 elxp4 4808 elxp5 4809 f1eq123d 5121 foeq123d 5122 f1oeq123d 5123 ofrfval 5720 eloprabi 5822 smoeq 5905 ecidg 6170 enqbreq2 6455 ltanqg 6498 caucvgprprlemexb 6805 caucvgsrlemgt1 6879 caucvgsrlemoffres 6884 ltrennb 6930 apneg 7602 mulext1 7603 ltdiv23 7858 lediv23 7859 halfpos 8156 addltmul 8161 div4p1lem1div2 8177 ztri3or 8288 iccf1o 8872 fzshftral 8970 fzoshftral 9094 2tnp1ge0ge0 9143 cjap 9506 |
Copyright terms: Public domain | W3C validator |