![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > 3bitrd | Unicode 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: ![]() ![]() |
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 3033 sbcnel12g 3089 elxp4 5134 elxp5 5135 f1eq123d 5472 foeq123d 5473 f1oeq123d 5474 fnmptfvd 5641 ofrfval 6115 eloprabi 6221 fnmpoovd 6240 smoeq 6315 ecidg 6625 ixpsnval 6727 enqbreq2 7386 ltanqg 7429 caucvgprprlemexb 7736 caucvgsrlemgt1 7824 caucvgsrlemoffres 7829 ltrennb 7883 apneg 8598 mulext1 8599 apdivmuld 8800 ltdiv23 8879 lediv23 8880 halfpos 9180 addltmul 9185 div4p1lem1div2 9202 ztri3or 9326 supminfex 9627 iccf1o 10034 fzshftral 10138 fzoshftral 10268 2tnp1ge0ge0 10332 fihashen1 10811 seq3coll 10854 cjap 10947 negfi 11268 tanaddaplem 11778 dvdssub 11877 addmodlteqALT 11897 dvdsmod 11900 oddp1even 11913 nn0o1gt2 11942 nn0oddm1d2 11946 infssuzex 11982 cncongr1 12135 cncongr2 12136 4sqlem11 12433 4sqlem17 12439 intopsn 12843 sgrp1 12874 sgrppropd 12876 issubg 13112 nmzsubg 13149 conjnmzb 13219 srg1zr 13341 ring1 13411 issubrg 13568 elmopn 14406 metss 14454 comet 14459 xmetxp 14467 limcmpted 14592 cnlimc 14601 lgsneg 14886 lgsne0 14900 lgsprme0 14904 |
Copyright terms: Public domain | W3C validator |