![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > bitr3di | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 25-Nov-1994.) |
Ref | Expression |
---|---|
bitr3di.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
bitr3di.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
bitr3di |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr3di.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | bicomi 131 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
3 | bitr3di.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | syl5rbb 192 |
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 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: xordc 1371 sbal2 1997 eqsnm 3714 fnressn 5646 fressnfv 5647 eluniimadm 5706 genpassl 7423 genpassu 7424 1idprl 7489 1idpru 7490 axcaucvglemres 7798 negeq0 8108 muleqadd 8521 crap0 8808 addltmul 9048 fzrev 9964 modq0 10206 cjap0 10784 cjne0 10785 caucvgrelemrec 10856 lenegsq 10972 isumss 11265 fsumsplit 11281 sumsplitdc 11306 dvdsabseq 11712 oddennn 12072 metrest 12845 elabgf0 13289 |
Copyright terms: Public domain | W3C validator |