Metamath Proof Explorer
Description: A syllogism inference from two biconditionals. Old name for bitrdi .
(Contributed by NM, 12-Mar-1993) (New usage is discouraged.)
|
|
Ref |
Expression |
|
Hypotheses |
syl6bb.1 |
|
|
|
syl6bb.2 |
|
|
Assertion |
syl6bb |
|
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
syl6bb.1 |
|
2 |
|
syl6bb.2 |
|
3 |
2
|
a1i |
|
4 |
1 3
|
bitrd |
|