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 186 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
4 | 3bitrd.3 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
5 | 3, 4 | bitrd 186 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜏)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: sbceqal 2869 sbcnel12g 2923 elxp4 4828 elxp5 4829 f1eq123d 5141 foeq123d 5142 f1oeq123d 5143 ofrfval 5740 eloprabi 5842 smoeq 5928 ecidg 6193 enqbreq2 6547 ltanqg 6590 caucvgprprlemexb 6897 caucvgsrlemgt1 6971 caucvgsrlemoffres 6976 ltrennb 7022 apneg 7711 mulext1 7712 ltdiv23 7970 lediv23 7971 halfpos 8262 addltmul 8267 div4p1lem1div2 8284 ztri3or 8394 supminfex 8685 iccf1o 9026 fzshftral 9125 fzoshftral 9247 2tnp1ge0ge0 9303 cjap 9793 negfi 10110 dvdssub 10240 addmodlteqALT 10259 dvdsmod 10262 oddp1even 10275 nn0o1gt2 10305 nn0oddm1d2 10309 infssuzex 10345 cncongr1 10485 cncongr2 10486 |
Copyright terms: Public domain | W3C validator |