![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > syl5bbr | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
syl5bbr.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
syl5bbr.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
syl5bbr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5bbr.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomi 123 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | syl5bbr.2 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl5bb 181 |
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: 3bitr3g 211 ianordc 798 19.16 1444 19.19 1553 cbvab 2157 necon1bbiidc 2260 elabgt 2678 sbceq1a 2767 sbcralt 2828 sbcrext 2829 sbccsbg 2872 sbccsb2g 2873 iunpw 4177 tfis 4249 xp11m 4702 ressn 4801 fnssresb 4954 fun11iun 5090 funimass4 5167 dffo4 5258 f1ompt 5263 fliftf 5382 resoprab2 5540 ralrnmpt2 5557 rexrnmpt2 5558 1stconst 5784 2ndconst 5785 dfsmo2 5843 smoiso 5858 brecop 6132 prarloclemn 6482 reapti 7363 indstr 8312 iccneg 8627 |
Copyright terms: Public domain | W3C validator |