Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > bitr2di | Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.) |
Ref | Expression |
---|---|
bitr2di.1 | |
bitr2di.2 |
Ref | Expression |
---|---|
bitr2di |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | bitr2di.1 | . . 3 | |
2 | bitr2di.2 | . . 3 | |
3 | 1, 2 | bitrdi 195 | . 2 |
4 | 3 | bicomd 140 | 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: bitr4id 198 bibif 693 pm5.61 789 oranabs 810 pm5.7dc 949 nbbndc 1389 resopab2 4938 xpcom 5157 f1od2 6214 map1 6790 ac6sfi 6876 elznn0 9227 rexuz3 10954 xrmaxiflemcom 11212 metrest 13300 sincosq3sgn 13543 sincosq4sgn 13544 |
Copyright terms: Public domain | W3C validator |