![]() |
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 187 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3bitrd.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 3, 4 | bitrd 187 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sbceqal 2916 sbcnel12g 2970 elxp4 4962 elxp5 4963 f1eq123d 5296 foeq123d 5297 f1oeq123d 5298 ofrfval 5922 eloprabi 6024 fnmpoovd 6042 smoeq 6117 ecidg 6423 ixpsnval 6525 enqbreq2 7066 ltanqg 7109 caucvgprprlemexb 7416 caucvgsrlemgt1 7490 caucvgsrlemoffres 7495 ltrennb 7541 apneg 8239 mulext1 8240 apdivmuld 8434 ltdiv23 8508 lediv23 8509 halfpos 8803 addltmul 8808 div4p1lem1div2 8825 ztri3or 8949 supminfex 9242 iccf1o 9628 fzshftral 9729 fzoshftral 9856 2tnp1ge0ge0 9915 fihashen1 10386 seq3coll 10426 cjap 10519 negfi 10838 tanaddaplem 11243 dvdssub 11333 addmodlteqALT 11352 dvdsmod 11355 oddp1even 11368 nn0o1gt2 11397 nn0oddm1d2 11401 infssuzex 11437 cncongr1 11577 cncongr2 11578 elmopn 12374 metss 12422 comet 12427 |
Copyright terms: Public domain | W3C validator |