![]() |
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 3018 sbcnel12g 3074 elxp4 5115 elxp5 5116 f1eq123d 5452 foeq123d 5453 f1oeq123d 5454 fnmptfvd 5619 ofrfval 6088 eloprabi 6194 fnmpoovd 6213 smoeq 6288 ecidg 6596 ixpsnval 6698 enqbreq2 7353 ltanqg 7396 caucvgprprlemexb 7703 caucvgsrlemgt1 7791 caucvgsrlemoffres 7796 ltrennb 7850 apneg 8564 mulext1 8565 apdivmuld 8766 ltdiv23 8845 lediv23 8846 halfpos 9146 addltmul 9151 div4p1lem1div2 9168 ztri3or 9292 supminfex 9593 iccf1o 10000 fzshftral 10103 fzoshftral 10233 2tnp1ge0ge0 10296 fihashen1 10772 seq3coll 10815 cjap 10908 negfi 11229 tanaddaplem 11739 dvdssub 11838 addmodlteqALT 11857 dvdsmod 11860 oddp1even 11873 nn0o1gt2 11902 nn0oddm1d2 11906 infssuzex 11942 cncongr1 12095 cncongr2 12096 intopsn 12718 sgrp1 12748 issubg 12964 nmzsubg 13001 srg1zr 13101 ring1 13167 issubrg 13280 elmopn 13817 metss 13865 comet 13870 xmetxp 13878 limcmpted 14003 cnlimc 14012 lgsneg 14296 lgsne0 14310 lgsprme0 14314 |
Copyright terms: Public domain | W3C validator |