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 131 | . 2 |
3 | syl5bbr.2 | . 2 | |
4 | 2, 3 | syl5bb 191 | 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: 3bitr3g 221 ianordc 869 19.16 1519 19.19 1629 cbvab 2240 necon1bbiidc 2346 rspc2gv 2775 elabgt 2799 sbceq1a 2891 sbcralt 2957 sbcrext 2958 sbccsbg 3001 sbccsb2g 3002 iunpw 4371 tfis 4467 xp11m 4947 ressn 5049 fnssresb 5205 fun11iun 5356 funimass4 5440 dffo4 5536 f1ompt 5539 fliftf 5668 resoprab2 5836 ralrnmpo 5853 rexrnmpo 5854 1stconst 6086 2ndconst 6087 dfsmo2 6152 smoiso 6167 brecop 6487 ixpsnf1o 6598 ac6sfi 6760 ismkvnex 6997 prarloclemn 7275 axcaucvglemres 7675 reapti 8309 indstr 9356 iccneg 9740 sqap0 10327 sqrt00 10780 minclpr 10976 absefib 11404 efieq1re 11405 prmind2 11728 sincosq3sgn 12836 sincosq4sgn 12837 |
Copyright terms: Public domain | W3C validator |