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: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sbceqal 2936 sbcnel12g 2990 elxp4 4996 elxp5 4997 f1eq123d 5330 foeq123d 5331 f1oeq123d 5332 ofrfval 5958 eloprabi 6062 fnmpoovd 6080 smoeq 6155 ecidg 6461 ixpsnval 6563 enqbreq2 7133 ltanqg 7176 caucvgprprlemexb 7483 caucvgsrlemgt1 7571 caucvgsrlemoffres 7576 ltrennb 7630 apneg 8340 mulext1 8341 apdivmuld 8540 ltdiv23 8614 lediv23 8615 halfpos 8909 addltmul 8914 div4p1lem1div2 8931 ztri3or 9055 supminfex 9348 iccf1o 9742 fzshftral 9843 fzoshftral 9970 2tnp1ge0ge0 10029 fihashen1 10500 seq3coll 10540 cjap 10633 negfi 10954 tanaddaplem 11359 dvdssub 11450 addmodlteqALT 11469 dvdsmod 11472 oddp1even 11485 nn0o1gt2 11514 nn0oddm1d2 11518 infssuzex 11554 cncongr1 11696 cncongr2 11697 elmopn 12526 metss 12574 comet 12579 xmetxp 12587 limcmpted 12712 cnlimc 12721 |
Copyright terms: Public domain | W3C validator |