| 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 188 | . 2 ⊢ (𝜑 → (𝜓 ↔ 𝜃)) |
| 4 | 3bitrd.3 | . 2 ⊢ (𝜑 → (𝜃 ↔ 𝜏)) | |
| 5 | 3, 4 | bitrd 188 | 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: sbceqal 3053 sbcnel12g 3109 elxp4 5167 elxp5 5168 f1eq123d 5508 foeq123d 5509 f1oeq123d 5510 fnmptfvd 5678 ofrfval 6157 eloprabi 6272 fnmpoovd 6291 smoeq 6366 ecidg 6676 ixpsnval 6778 enqbreq2 7452 ltanqg 7495 caucvgprprlemexb 7802 caucvgsrlemgt1 7890 caucvgsrlemoffres 7895 ltrennb 7949 apneg 8666 mulext1 8667 apdivmuld 8868 ltdiv23 8947 lediv23 8948 halfpos 9250 addltmul 9256 div4p1lem1div2 9273 ztri3or 9397 supminfex 9700 iccf1o 10108 fzshftral 10212 fzoshftral 10348 infssuzex 10357 2tnp1ge0ge0 10425 fihashen1 10925 seq3coll 10968 cjap 11136 negfi 11458 tanaddaplem 11968 dvdssub 12068 addmodlteqALT 12089 dvdsmod 12092 oddp1even 12106 nn0o1gt2 12135 nn0oddm1d2 12139 bitscmp 12188 cncongr1 12344 cncongr2 12345 4sqlem11 12643 4sqlem17 12649 intopsn 13117 sgrp1 13161 sgrppropd 13163 issubg 13427 nmzsubg 13464 conjnmzb 13534 srg1zr 13667 ring1 13739 issubrg 13901 znf1o 14331 znleval 14333 znunit 14339 elmopn 14836 metss 14884 comet 14889 xmetxp 14897 limcmpted 15053 cnlimc 15062 lgsneg 15419 lgsne0 15433 lgsprme0 15437 lgsquadlem1 15472 lgsquadlem2 15473 2lgs 15499 2lgsoddprm 15508 |
| Copyright terms: Public domain | W3C validator |