Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > sylnib | Unicode version |
Description: A mixed syllogism inference from an implication and a biconditional. (Contributed by Wolf Lammen, 16-Dec-2013.) |
Ref | Expression |
---|---|
sylnib.1 | |
sylnib.2 |
Ref | Expression |
---|---|
sylnib |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sylnib.1 | . 2 | |
2 | sylnib.2 | . . 3 | |
3 | 2 | a1i 9 | . 2 |
4 | 1, 3 | mtbid 662 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 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 ax-in1 604 ax-in2 605 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylnibr 667 neqcomd 2169 inssdif0im 3471 undifexmid 4166 ordtriexmidlem2 4491 dmsn0el 5067 fidifsnen 6827 ctssdccl 7067 onntri35 7184 onntri45 7188 ltpopr 7527 caucvgprprlemnbj 7625 xrlttri3 9724 fzneuz 10026 iseqf1olemqcl 10411 iseqf1olemnab 10413 iseqf1olemab 10414 exp3val 10447 pwle2 13719 |
Copyright terms: Public domain | W3C validator |