![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl6bbr | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl6bbr.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
syl6bbr.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl6bbr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl6bbr.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | syl6bbr.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 123 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | syl6bb 185 |
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 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: 3bitr4g 212 bibi2i 216 equsalh 1611 eueq3dc 2709 sbcel12g 2859 sbceqg 2860 sbcnel12g 2861 reldisj 3265 r19.3rm 3304 rabxp 4323 elrng 4469 iss 4597 eliniseg 4638 fcnvres 5016 dffv3g 5117 funimass4 5167 fndmdif 5215 fneqeql 5218 funimass3 5226 elrnrexdmb 5250 dff4im 5256 fconst4m 5324 elunirn 5348 riota1 5429 riota2df 5431 f1ocnvfv3 5444 eqfnov 5549 caoftrn 5678 mpt2xopovel 5797 rntpos 5813 ordgt0ge1 5957 iinerm 6114 erinxp 6116 qliftfun 6124 indpi 6326 genpdflem 6490 genpdisj 6506 genpassl 6507 genpassu 6508 ltpopr 6569 ltexprlemm 6574 ltexprlemdisj 6580 ltexprlemloc 6581 letri3 6896 letr 6898 ltneg 7252 leneg 7255 reapltxor 7373 apsym 7390 elnnnn0 8001 zrevaddcl 8071 znnsub 8072 znn0sub 8085 prime 8113 eluz2 8255 eluz2b1 8315 nn01to3 8328 qrevaddcl 8353 xrletri3 8491 xrletr 8494 iccid 8564 elicopnf 8608 fzsplit2 8684 fzsn 8699 fzpr 8709 uzsplit 8724 lt2sqi 8994 le2sqi 8995 bj-sseq 9266 |
Copyright terms: Public domain | W3C validator |