![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > sylnibr | Unicode version |
Description: A mixed syllogism inference from an implication and a biconditional. Useful for substituting an consequent with a definition. (Contributed by Wolf Lammen, 16-Dec-2013.) |
Ref | Expression |
---|---|
sylnibr.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
sylnibr.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
sylnibr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylnibr.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | sylnibr.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | bicomi 132 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() |
4 | 1, 3 | sylnib 676 |
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 106 ax-ia2 107 ax-ia3 108 ax-in1 614 ax-in2 615 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: rexnalim 2466 nssr 3216 difdif 3261 unssin 3375 inssun 3376 undif3ss 3397 ssdif0im 3488 dcun 3534 prneimg 3775 iundif2ss 3953 nssssr 4223 pofun 4313 frirrg 4351 regexmidlem1 4533 dcdifsnid 6505 unfidisj 6921 fidcenumlemrks 6952 difinfsn 7099 pw1nel3 7230 addnqprlemfl 7558 addnqprlemfu 7559 mulnqprlemfl 7574 mulnqprlemfu 7575 cauappcvgprlemladdru 7655 caucvgprprlemaddq 7707 fzpreddisj 10071 fprodntrivap 11592 pw2dvdslemn 12165 isnsgrp 12812 ivthinclemdisj 14121 lgseisenlem1 14453 pwtrufal 14750 pw1nct 14755 nninfsellemsuc 14764 |
Copyright terms: Public domain | W3C validator |