Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > syl5rbb | Structured version Visualization version Unicode version |
Description: A syllogism inference from two biconditionals. (Contributed by NM, 1-Aug-1993.) |
Ref | Expression |
---|---|
syl5rbb.1 | |
syl5rbb.2 |
Ref | Expression |
---|---|
syl5rbb |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | syl5rbb.1 | . . 3 | |
2 | syl5rbb.2 | . . 3 | |
3 | 1, 2 | syl5bb 272 | . 2 |
4 | 3 | bicomd 213 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wb 196 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 197 |
This theorem is referenced by: syl5rbbr 275 necon1abid 2832 necon4abid 2834 uniiunlem 3691 r19.9rzv 4065 inimasn 5550 fnresdisj 6001 f1oiso 6601 reldm 7219 rdglim2 7528 mptelixpg 7945 1idpr 9851 nndiv 11061 fz1sbc 12416 grpid 17457 znleval 19903 fbunfip 21673 lmflf 21809 metcld2 23105 lgsne0 25060 isuvtxa 26295 clwwlksnun 26974 frgrncvvdeqlem2 27164 isph 27677 ofpreima 29465 eulerpartlemd 30428 bnj168 30798 opelco3 31678 wl-2sb6d 33341 poimirlem26 33435 cnambfre 33458 heibor1 33609 opltn0 34477 cvrnbtwn2 34562 cvrnbtwn4 34566 atlltn0 34593 pmapjat1 35139 dih1dimatlem 36618 2rexfrabdioph 37360 dnwech 37618 rfovcnvf1od 38298 uneqsn 38321 csbabgOLD 39050 2reu4a 41189 lighneallem2 41523 isrnghm 41892 rnghmval2 41895 |
Copyright terms: Public domain | W3C validator |